Locally integrable functions #
A function is called locally integrable (MeasureTheory.LocallyIntegrable) if it is integrable
on a neighborhood of every point. More generally, it is locally integrable on s if it is
locally integrable on a neighbourhood within s of any point of s.
This file contains properties of locally integrable functions, and integrability results on compact sets.
Main statements #
Continuous.locallyIntegrable: A continuous function is locally integrable.ContinuousOn.locallyIntegrableOn: A function which is continuous onsis locally integrable ons.
def
MeasureTheory.LocallyIntegrableOn
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
(f : X → E)
(s : Set X)
(μ : autoParam (MeasureTheory.Measure X) _auto✝)
:
A function f : X → E is locally integrable on s, for s ⊆ X, if for every x ∈ s there is
a neighbourhood of x within s on which f is integrable. (Note this is, in general, strictly
weaker than local integrability with respect to μ.restrict s.)
Equations
- MeasureTheory.LocallyIntegrableOn f s = ∀ (x : X), x ∈ s → MeasureTheory.IntegrableAtFilter f (nhdsWithin x s)
Instances For
theorem
MeasureTheory.LocallyIntegrableOn.mono
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{s : Set X}
(hf : MeasureTheory.LocallyIntegrableOn f s)
{t : Set X}
(hst : t ⊆ s)
:
theorem
MeasureTheory.LocallyIntegrableOn.norm
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{s : Set X}
(hf : MeasureTheory.LocallyIntegrableOn f s)
:
MeasureTheory.LocallyIntegrableOn (fun x => ‖f x‖) s
theorem
MeasureTheory.IntegrableOn.locallyIntegrableOn
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{s : Set X}
(hf : MeasureTheory.IntegrableOn f s)
:
theorem
MeasureTheory.LocallyIntegrableOn.integrableOn_isCompact
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{s : Set X}
(hf : MeasureTheory.LocallyIntegrableOn f s)
(hs : IsCompact s)
:
If a function is locally integrable on a compact set, then it is integrable on that set.
theorem
MeasureTheory.LocallyIntegrableOn.integrableOn_compact_subset
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{s : Set X}
(hf : MeasureTheory.LocallyIntegrableOn f s)
{t : Set X}
(hst : t ⊆ s)
(ht : IsCompact t)
:
theorem
MeasureTheory.LocallyIntegrableOn.exists_countable_integrableOn
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{s : Set X}
[TopologicalSpace.SecondCountableTopology X]
(hf : MeasureTheory.LocallyIntegrableOn f s)
:
If a function f is locally integrable on a set s in a second countable topological space,
then there exist countably many open sets u covering s such that f is integrable on each
set u ∩ s.
theorem
MeasureTheory.LocallyIntegrableOn.exists_nat_integrableOn
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{s : Set X}
[TopologicalSpace.SecondCountableTopology X]
(hf : MeasureTheory.LocallyIntegrableOn f s)
:
If a function f is locally integrable on a set s in a second countable topological space,
then there exists a sequence of open sets u n covering s such that f is integrable on each
set u n ∩ s.
theorem
MeasureTheory.LocallyIntegrableOn.aestronglyMeasurable
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{s : Set X}
[TopologicalSpace.SecondCountableTopology X]
(hf : MeasureTheory.LocallyIntegrableOn f s)
:
theorem
MeasureTheory.locallyIntegrableOn_iff
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{s : Set X}
[LocallyCompactSpace X]
[T2Space X]
(hs : IsClosed s ∨ IsOpen s)
:
MeasureTheory.LocallyIntegrableOn f s ↔ ∀ (k : Set X), k ⊆ s → IsCompact k → MeasureTheory.IntegrableOn f k
If s is either open, or closed, then f is locally integrable on s iff it is integrable on
every compact subset contained in s.
theorem
MeasureTheory.LocallyIntegrableOn.add
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{g : X → E}
{μ : MeasureTheory.Measure X}
{s : Set X}
(hf : MeasureTheory.LocallyIntegrableOn f s)
(hg : MeasureTheory.LocallyIntegrableOn g s)
:
MeasureTheory.LocallyIntegrableOn (f + g) s
theorem
MeasureTheory.LocallyIntegrableOn.sub
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{g : X → E}
{μ : MeasureTheory.Measure X}
{s : Set X}
(hf : MeasureTheory.LocallyIntegrableOn f s)
(hg : MeasureTheory.LocallyIntegrableOn g s)
:
MeasureTheory.LocallyIntegrableOn (f - g) s
theorem
MeasureTheory.LocallyIntegrableOn.neg
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{s : Set X}
(hf : MeasureTheory.LocallyIntegrableOn f s)
:
def
MeasureTheory.LocallyIntegrable
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
(f : X → E)
(μ : autoParam (MeasureTheory.Measure X) _auto✝)
:
A function f : X → E is locally integrable if it is integrable on a neighborhood of every
point. In particular, it is integrable on all compact sets,
see LocallyIntegrable.integrableOn_isCompact.
Equations
- MeasureTheory.LocallyIntegrable f = ∀ (x : X), MeasureTheory.IntegrableAtFilter f (nhds x)
Instances For
theorem
MeasureTheory.locallyIntegrableOn_univ
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
:
theorem
MeasureTheory.LocallyIntegrable.locallyIntegrableOn
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
(hf : MeasureTheory.LocallyIntegrable f)
(s : Set X)
:
theorem
MeasureTheory.Integrable.locallyIntegrable
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
(hf : MeasureTheory.Integrable f)
:
theorem
MeasureTheory.locallyIntegrableOn_of_locallyIntegrable_restrict
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{s : Set X}
[OpensMeasurableSpace X]
(hf : MeasureTheory.LocallyIntegrable f)
:
If f is locally integrable with respect to μ.restrict s, it is locally integrable on s.
(See locallyIntegrableOn_iff_locallyIntegrable_restrict for an iff statement when s is
closed.)
theorem
MeasureTheory.locallyIntegrableOn_iff_locallyIntegrable_restrict
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{s : Set X}
[OpensMeasurableSpace X]
(hs : IsClosed s)
:
If s is closed, being locally integrable on s wrt μ is equivalent to being locally
integrable with respect to μ.restrict s. For the one-way implication without assuming s closed,
see locallyIntegrableOn_of_locallyIntegrable_restrict.
theorem
MeasureTheory.LocallyIntegrable.integrableOn_isCompact
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{k : Set X}
(hf : MeasureTheory.LocallyIntegrable f)
(hk : IsCompact k)
:
If a function is locally integrable, then it is integrable on any compact set.
theorem
MeasureTheory.LocallyIntegrable.integrableOn_nhds_isCompact
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
(hf : MeasureTheory.LocallyIntegrable f)
{k : Set X}
(hk : IsCompact k)
:
∃ u, IsOpen u ∧ k ⊆ u ∧ MeasureTheory.IntegrableOn f u
If a function is locally integrable, then it is integrable on an open neighborhood of any compact set.
theorem
MeasureTheory.locallyIntegrable_iff
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[LocallyCompactSpace X]
:
MeasureTheory.LocallyIntegrable f ↔ ∀ (k : Set X), IsCompact k → MeasureTheory.IntegrableOn f k
theorem
MeasureTheory.LocallyIntegrable.aestronglyMeasurable
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[TopologicalSpace.SecondCountableTopology X]
(hf : MeasureTheory.LocallyIntegrable f)
:
theorem
MeasureTheory.LocallyIntegrable.exists_nat_integrableOn
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[TopologicalSpace.SecondCountableTopology X]
(hf : MeasureTheory.LocallyIntegrable f)
:
If a function is locally integrable in a second countable topological space, then there exists a sequence of open sets covering the space on which it is integrable.
theorem
MeasureTheory.Memℒp.locallyIntegrable
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure X}
[MeasureTheory.IsLocallyFiniteMeasure μ]
{f : X → E}
{p : ENNReal}
(hf : MeasureTheory.Memℒp f p)
(hp : 1 ≤ p)
:
theorem
MeasureTheory.locallyIntegrable_const
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure X}
[MeasureTheory.IsLocallyFiniteMeasure μ]
(c : E)
:
MeasureTheory.LocallyIntegrable fun x => c
theorem
MeasureTheory.locallyIntegrableOn_const
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure X}
{s : Set X}
[MeasureTheory.IsLocallyFiniteMeasure μ]
(c : E)
:
MeasureTheory.LocallyIntegrableOn (fun x => c) s
theorem
MeasureTheory.locallyIntegrable_zero
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure X}
:
MeasureTheory.LocallyIntegrable fun x => 0
theorem
MeasureTheory.locallyIntegrableOn_zero
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure X}
{s : Set X}
:
MeasureTheory.LocallyIntegrableOn (fun x => 0) s
theorem
MeasureTheory.LocallyIntegrable.indicator
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
(hf : MeasureTheory.LocallyIntegrable f)
{s : Set X}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.locallyIntegrable_map_homeomorph
{X : Type u_1}
{Y : Type u_2}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[MeasurableSpace Y]
[TopologicalSpace Y]
[NormedAddCommGroup E]
[BorelSpace X]
[BorelSpace Y]
(e : X ≃ₜ Y)
{f : Y → E}
{μ : MeasureTheory.Measure X}
:
theorem
MeasureTheory.LocallyIntegrable.add
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{g : X → E}
{μ : MeasureTheory.Measure X}
(hf : MeasureTheory.LocallyIntegrable f)
(hg : MeasureTheory.LocallyIntegrable g)
:
theorem
MeasureTheory.LocallyIntegrable.sub
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{g : X → E}
{μ : MeasureTheory.Measure X}
(hf : MeasureTheory.LocallyIntegrable f)
(hg : MeasureTheory.LocallyIntegrable g)
:
theorem
MeasureTheory.LocallyIntegrable.neg
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
(hf : MeasureTheory.LocallyIntegrable f)
:
theorem
MeasureTheory.LocallyIntegrable.smul
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{𝕜 : Type u_5}
[NormedAddCommGroup 𝕜]
[SMulZeroClass 𝕜 E]
[BoundedSMul 𝕜 E]
(hf : MeasureTheory.LocallyIntegrable f)
(c : 𝕜)
:
theorem
MeasureTheory.locallyIntegrable_finset_sum'
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure X}
{ι : Type u_5}
(s : Finset ι)
{f : ι → X → E}
(hf : ∀ (i : ι), i ∈ s → MeasureTheory.LocallyIntegrable (f i))
:
MeasureTheory.LocallyIntegrable (Finset.sum s fun i => f i)
theorem
MeasureTheory.locallyIntegrable_finset_sum
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure X}
{ι : Type u_5}
(s : Finset ι)
{f : ι → X → E}
(hf : ∀ (i : ι), i ∈ s → MeasureTheory.LocallyIntegrable (f i))
:
MeasureTheory.LocallyIntegrable fun a => Finset.sum s fun i => f i a
theorem
MeasureTheory.LocallyIntegrable.integrable_smul_left_of_hasCompactSupport
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[NormedSpace ℝ E]
[OpensMeasurableSpace X]
[T2Space X]
(hf : MeasureTheory.LocallyIntegrable f)
{g : X → ℝ}
(hg : Continuous g)
(h'g : HasCompactSupport g)
:
MeasureTheory.Integrable fun x => g x • f x
If f is locally integrable and g is continuous with compact support,
then g • f is integrable.
theorem
MeasureTheory.LocallyIntegrable.integrable_smul_right_of_hasCompactSupport
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure X}
[NormedSpace ℝ E]
[OpensMeasurableSpace X]
[T2Space X]
{f : X → ℝ}
(hf : MeasureTheory.LocallyIntegrable f)
{g : X → E}
(hg : Continuous g)
(h'g : HasCompactSupport g)
:
MeasureTheory.Integrable fun x => f x • g x
If f is locally integrable and g is continuous with compact support,
then f • g is integrable.
theorem
Continuous.locallyIntegrable
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[OpensMeasurableSpace X]
[MeasureTheory.IsLocallyFiniteMeasure μ]
[SecondCountableTopologyEither X E]
(hf : Continuous f)
:
A continuous function f is locally integrable with respect to any locally finite measure.
theorem
ContinuousOn.locallyIntegrableOn
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[OpensMeasurableSpace X]
[MeasureTheory.IsLocallyFiniteMeasure μ]
{K : Set X}
[SecondCountableTopologyEither X E]
(hf : ContinuousOn f K)
(hK : MeasurableSet K)
:
A function f continuous on a set K is locally integrable on this set with respect
to any locally finite measure.
theorem
ContinuousOn.integrableOn_compact
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[OpensMeasurableSpace X]
[MeasureTheory.IsLocallyFiniteMeasure μ]
{K : Set X}
[TopologicalSpace.MetrizableSpace X]
(hK : IsCompact K)
(hf : ContinuousOn f K)
:
A function f continuous on a compact set K is integrable on this set with respect to any
locally finite measure.
theorem
ContinuousOn.integrableOn_Icc
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[OpensMeasurableSpace X]
[MeasureTheory.IsLocallyFiniteMeasure μ]
{a : X}
{b : X}
[TopologicalSpace.MetrizableSpace X]
[Preorder X]
[CompactIccSpace X]
(hf : ContinuousOn f (Set.Icc a b))
:
MeasureTheory.IntegrableOn f (Set.Icc a b)
theorem
Continuous.integrableOn_Icc
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[OpensMeasurableSpace X]
[MeasureTheory.IsLocallyFiniteMeasure μ]
{a : X}
{b : X}
[TopologicalSpace.MetrizableSpace X]
[Preorder X]
[CompactIccSpace X]
(hf : Continuous f)
:
MeasureTheory.IntegrableOn f (Set.Icc a b)
theorem
Continuous.integrableOn_Ioc
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[OpensMeasurableSpace X]
[MeasureTheory.IsLocallyFiniteMeasure μ]
{a : X}
{b : X}
[TopologicalSpace.MetrizableSpace X]
[Preorder X]
[CompactIccSpace X]
(hf : Continuous f)
:
MeasureTheory.IntegrableOn f (Set.Ioc a b)
theorem
ContinuousOn.integrableOn_uIcc
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[OpensMeasurableSpace X]
[MeasureTheory.IsLocallyFiniteMeasure μ]
{a : X}
{b : X}
[TopologicalSpace.MetrizableSpace X]
[LinearOrder X]
[CompactIccSpace X]
(hf : ContinuousOn f (Set.uIcc a b))
:
MeasureTheory.IntegrableOn f (Set.uIcc a b)
theorem
Continuous.integrableOn_uIcc
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[OpensMeasurableSpace X]
[MeasureTheory.IsLocallyFiniteMeasure μ]
{a : X}
{b : X}
[TopologicalSpace.MetrizableSpace X]
[LinearOrder X]
[CompactIccSpace X]
(hf : Continuous f)
:
MeasureTheory.IntegrableOn f (Set.uIcc a b)
theorem
Continuous.integrableOn_uIoc
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[OpensMeasurableSpace X]
[MeasureTheory.IsLocallyFiniteMeasure μ]
{a : X}
{b : X}
[TopologicalSpace.MetrizableSpace X]
[LinearOrder X]
[CompactIccSpace X]
(hf : Continuous f)
:
MeasureTheory.IntegrableOn f (Ι a b)
theorem
Continuous.integrable_of_hasCompactSupport
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[OpensMeasurableSpace X]
[MeasureTheory.IsLocallyFiniteMeasure μ]
[TopologicalSpace.MetrizableSpace X]
(hf : Continuous f)
(hcf : HasCompactSupport f)
:
A continuous function with compact support is integrable on the whole space.
theorem
MonotoneOn.integrableOn_of_measure_ne_top
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{s : Set X}
[BorelSpace X]
[ConditionallyCompleteLinearOrder X]
[ConditionallyCompleteLinearOrder E]
[OrderTopology X]
[OrderTopology E]
[TopologicalSpace.SecondCountableTopology E]
(hmono : MonotoneOn f s)
{a : X}
{b : X}
(ha : IsLeast s a)
(hb : IsGreatest s b)
(hs : ↑↑μ s ≠ ⊤)
(h's : MeasurableSet s)
:
theorem
MonotoneOn.integrableOn_isCompact
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{s : Set X}
[BorelSpace X]
[ConditionallyCompleteLinearOrder X]
[ConditionallyCompleteLinearOrder E]
[OrderTopology X]
[OrderTopology E]
[TopologicalSpace.SecondCountableTopology E]
[MeasureTheory.IsFiniteMeasureOnCompacts μ]
(hs : IsCompact s)
(hmono : MonotoneOn f s)
:
theorem
AntitoneOn.integrableOn_of_measure_ne_top
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{s : Set X}
[BorelSpace X]
[ConditionallyCompleteLinearOrder X]
[ConditionallyCompleteLinearOrder E]
[OrderTopology X]
[OrderTopology E]
[TopologicalSpace.SecondCountableTopology E]
(hanti : AntitoneOn f s)
{a : X}
{b : X}
(ha : IsLeast s a)
(hb : IsGreatest s b)
(hs : ↑↑μ s ≠ ⊤)
(h's : MeasurableSet s)
:
theorem
AntioneOn.integrableOn_isCompact
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{s : Set X}
[BorelSpace X]
[ConditionallyCompleteLinearOrder X]
[ConditionallyCompleteLinearOrder E]
[OrderTopology X]
[OrderTopology E]
[TopologicalSpace.SecondCountableTopology E]
[MeasureTheory.IsFiniteMeasureOnCompacts μ]
(hs : IsCompact s)
(hanti : AntitoneOn f s)
:
theorem
Monotone.locallyIntegrable
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[BorelSpace X]
[ConditionallyCompleteLinearOrder X]
[ConditionallyCompleteLinearOrder E]
[OrderTopology X]
[OrderTopology E]
[TopologicalSpace.SecondCountableTopology E]
[MeasureTheory.IsLocallyFiniteMeasure μ]
(hmono : Monotone f)
:
theorem
Antitone.locallyIntegrable
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[BorelSpace X]
[ConditionallyCompleteLinearOrder X]
[ConditionallyCompleteLinearOrder E]
[OrderTopology X]
[OrderTopology E]
[TopologicalSpace.SecondCountableTopology E]
[MeasureTheory.IsLocallyFiniteMeasure μ]
(hanti : Antitone f)
:
theorem
MeasureTheory.IntegrableOn.mul_continuousOn_of_subset
{X : Type u_1}
{R : Type u_4}
[MeasurableSpace X]
[TopologicalSpace X]
{μ : MeasureTheory.Measure X}
[OpensMeasurableSpace X]
{A : Set X}
{K : Set X}
[NormedRing R]
[SecondCountableTopologyEither X R]
{g : X → R}
{g' : X → R}
(hg : MeasureTheory.IntegrableOn g A)
(hg' : ContinuousOn g' K)
(hA : MeasurableSet A)
(hK : IsCompact K)
(hAK : A ⊆ K)
:
MeasureTheory.IntegrableOn (fun x => g x * g' x) A
theorem
MeasureTheory.IntegrableOn.mul_continuousOn
{X : Type u_1}
{R : Type u_4}
[MeasurableSpace X]
[TopologicalSpace X]
{μ : MeasureTheory.Measure X}
[OpensMeasurableSpace X]
{K : Set X}
[NormedRing R]
[SecondCountableTopologyEither X R]
{g : X → R}
{g' : X → R}
[T2Space X]
(hg : MeasureTheory.IntegrableOn g K)
(hg' : ContinuousOn g' K)
(hK : IsCompact K)
:
MeasureTheory.IntegrableOn (fun x => g x * g' x) K
theorem
MeasureTheory.IntegrableOn.continuousOn_mul_of_subset
{X : Type u_1}
{R : Type u_4}
[MeasurableSpace X]
[TopologicalSpace X]
{μ : MeasureTheory.Measure X}
[OpensMeasurableSpace X]
{A : Set X}
{K : Set X}
[NormedRing R]
[SecondCountableTopologyEither X R]
{g : X → R}
{g' : X → R}
(hg : ContinuousOn g K)
(hg' : MeasureTheory.IntegrableOn g' A)
(hK : IsCompact K)
(hA : MeasurableSet A)
(hAK : A ⊆ K)
:
MeasureTheory.IntegrableOn (fun x => g x * g' x) A
theorem
MeasureTheory.IntegrableOn.continuousOn_mul
{X : Type u_1}
{R : Type u_4}
[MeasurableSpace X]
[TopologicalSpace X]
{μ : MeasureTheory.Measure X}
[OpensMeasurableSpace X]
{K : Set X}
[NormedRing R]
[SecondCountableTopologyEither X R]
{g : X → R}
{g' : X → R}
[T2Space X]
(hg : ContinuousOn g K)
(hg' : MeasureTheory.IntegrableOn g' K)
(hK : IsCompact K)
:
MeasureTheory.IntegrableOn (fun x => g x * g' x) K
theorem
MeasureTheory.IntegrableOn.continuousOn_smul
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure X}
[OpensMeasurableSpace X]
{K : Set X}
{𝕜 : Type u_5}
[NormedField 𝕜]
[NormedSpace 𝕜 E]
[T2Space X]
[SecondCountableTopologyEither X 𝕜]
{g : X → E}
(hg : MeasureTheory.IntegrableOn g K)
{f : X → 𝕜}
(hf : ContinuousOn f K)
(hK : IsCompact K)
:
MeasureTheory.IntegrableOn (fun x => f x • g x) K
theorem
MeasureTheory.IntegrableOn.smul_continuousOn
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure X}
[OpensMeasurableSpace X]
{K : Set X}
{𝕜 : Type u_5}
[NormedField 𝕜]
[NormedSpace 𝕜 E]
[T2Space X]
[SecondCountableTopologyEither X E]
{f : X → 𝕜}
(hf : MeasureTheory.IntegrableOn f K)
{g : X → E}
(hg : ContinuousOn g K)
(hK : IsCompact K)
:
MeasureTheory.IntegrableOn (fun x => f x • g x) K
theorem
MeasureTheory.LocallyIntegrableOn.continuousOn_mul
{X : Type u_1}
{R : Type u_4}
[MeasurableSpace X]
[TopologicalSpace X]
{μ : MeasureTheory.Measure X}
[OpensMeasurableSpace X]
[LocallyCompactSpace X]
[T2Space X]
[NormedRing R]
[SecondCountableTopologyEither X R]
{f : X → R}
{g : X → R}
{s : Set X}
(hf : MeasureTheory.LocallyIntegrableOn f s)
(hg : ContinuousOn g s)
(hs : IsOpen s)
:
MeasureTheory.LocallyIntegrableOn (fun x => g x * f x) s
theorem
MeasureTheory.LocallyIntegrableOn.mul_continuousOn
{X : Type u_1}
{R : Type u_4}
[MeasurableSpace X]
[TopologicalSpace X]
{μ : MeasureTheory.Measure X}
[OpensMeasurableSpace X]
[LocallyCompactSpace X]
[T2Space X]
[NormedRing R]
[SecondCountableTopologyEither X R]
{f : X → R}
{g : X → R}
{s : Set X}
(hf : MeasureTheory.LocallyIntegrableOn f s)
(hg : ContinuousOn g s)
(hs : IsOpen s)
:
MeasureTheory.LocallyIntegrableOn (fun x => f x * g x) s
theorem
MeasureTheory.LocallyIntegrableOn.continuousOn_smul
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure X}
[OpensMeasurableSpace X]
[LocallyCompactSpace X]
[T2Space X]
{𝕜 : Type u_5}
[NormedField 𝕜]
[SecondCountableTopologyEither X 𝕜]
[NormedSpace 𝕜 E]
{f : X → E}
{g : X → 𝕜}
{s : Set X}
(hs : IsOpen s)
(hf : MeasureTheory.LocallyIntegrableOn f s)
(hg : ContinuousOn g s)
:
MeasureTheory.LocallyIntegrableOn (fun x => g x • f x) s
theorem
MeasureTheory.LocallyIntegrableOn.smul_continuousOn
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure X}
[OpensMeasurableSpace X]
[LocallyCompactSpace X]
[T2Space X]
{𝕜 : Type u_5}
[NormedField 𝕜]
[SecondCountableTopologyEither X E]
[NormedSpace 𝕜 E]
{f : X → 𝕜}
{g : X → E}
{s : Set X}
(hs : IsOpen s)
(hf : MeasureTheory.LocallyIntegrableOn f s)
(hg : ContinuousOn g s)
:
MeasureTheory.LocallyIntegrableOn (fun x => f x • g x) s