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 on s is locally integrable on s.

def MeasureTheory.LocallyIntegrableOn {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] (f : X → ε) (s : Set X) (μ : Measure X := by volume_tac) : Prop

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 ∈ s, MeasureTheory.IntegrableAtFilter f (nhdsWithin x s) μ

theorem MeasureTheory.LocallyIntegrableOn.mono_set {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} {s : Set X} (hf : LocallyIntegrableOn f s μ) {t : Set X} (hst : t ⊆ s) : LocallyIntegrableOn f t μ

theorem MeasureTheory.LocallyIntegrableOn.enorm {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} {s : Set X} (hf : LocallyIntegrableOn f s μ) : LocallyIntegrableOn (fun (x : X) => ‖f x‖ₑ) s μ

theorem MeasureTheory.LocallyIntegrableOn.norm {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : Measure X} {s : Set X} {f : X → E} (hf : LocallyIntegrableOn f s μ) : LocallyIntegrableOn (fun (x : X) => ‖f x‖) s μ

theorem MeasureTheory.LocallyIntegrableOn.mono_enorm {X : Type u_1} {ε : Type u_3} {ε' : Type u_4} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] [TopologicalSpace ε'] [ContinuousENorm ε'] {f : X → ε} {μ : Measure X} {s : Set X} (hf : LocallyIntegrableOn f s μ) {g : X → ε'} (hg : AEStronglyMeasurable g μ) (h : ∀ᵐ (x : X) ∂μ, ‖g x‖ₑ ≤ ‖f x‖ₑ) : LocallyIntegrableOn g s μ

theorem MeasureTheory.LocallyIntegrableOn.mono {X : Type u_1} {E : Type u_6} {F : Type u_7} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] [NormedAddCommGroup F] {μ : Measure X} {s : Set X} {f : X → E} (hf : LocallyIntegrableOn f s μ) {g : X → F} (hg : AEStronglyMeasurable g μ) (h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖) : LocallyIntegrableOn g s μ

theorem MeasureTheory.IntegrableOn.locallyIntegrableOn {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} {s : Set X} (hf : IntegrableOn f s μ) : LocallyIntegrableOn f s μ

theorem MeasureTheory.LocallyIntegrableOn.integrableOn_isCompact {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} {s : Set X} [TopologicalSpace.PseudoMetrizableSpace ε] (hf : LocallyIntegrableOn f s μ) (hs : IsCompact s) : IntegrableOn f 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} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} {s : Set X} [TopologicalSpace.PseudoMetrizableSpace ε] (hf : LocallyIntegrableOn f s μ) {t : Set X} (hst : t ⊆ s) (ht : IsCompact t) : IntegrableOn f t μ

theorem MeasureTheory.LocallyIntegrableOn.exists_countable_integrableOn {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} {s : Set X} [SecondCountableTopology X] (hf : LocallyIntegrableOn f s μ) : ∃ (T : Set (Set X)), T.Countable ∧ (∀ u ∈ T, IsOpen u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, IntegrableOn f (u ∩ 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} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} {s : Set X} [SecondCountableTopology X] (hf : LocallyIntegrableOn f s μ) : ∃ (u : ℕ → Set X), (∀ (n : ℕ), IsOpen (u n)) ∧ s ⊆ ⋃ (n : ℕ), u n ∧ ∀ (n : ℕ), IntegrableOn f (u n ∩ 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} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} {s : Set X} [TopologicalSpace.PseudoMetrizableSpace ε] [SecondCountableTopology X] (hf : LocallyIntegrableOn f s μ) : AEStronglyMeasurable f (μ.restrict s)

theorem MeasureTheory.locallyIntegrableOn_iff {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} {s : Set X} [TopologicalSpace.PseudoMetrizableSpace ε] [LocallyCompactSpace X] (hs : IsLocallyClosed s) : LocallyIntegrableOn f s μ ↔ ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ

If s is locally closed (e.g. 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} {ε'' : Type u_5} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε''] [ESeminormedAddMonoid ε''] {μ : Measure X} {s : Set X} [ContinuousAdd ε''] {f g : X → ε''} (hf : LocallyIntegrableOn f s μ) (hg : LocallyIntegrableOn g s μ) : LocallyIntegrableOn (f + g) s μ

theorem MeasureTheory.LocallyIntegrableOn.sub {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : Measure X} {s : Set X} {f g : X → E} (hf : LocallyIntegrableOn f s μ) (hg : LocallyIntegrableOn g s μ) : LocallyIntegrableOn (f - g) s μ

theorem MeasureTheory.LocallyIntegrableOn.neg {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : Measure X} {s : Set X} {f : X → E} (hf : LocallyIntegrableOn f s μ) : LocallyIntegrableOn (-f) s μ

def MeasureTheory.LocallyIntegrable {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] (f : X → ε) (μ : Measure X := by volume_tac) : Prop

A function f : X → ε 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) μ

theorem MeasureTheory.locallyIntegrable_comap {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} {s : Set X} (hs : MeasurableSet s) : LocallyIntegrable (fun (x : ↑s) => f ↑x) (Measure.comap Subtype.val μ) ↔ LocallyIntegrableOn f s μ

theorem MeasureTheory.locallyIntegrableOn_univ {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} : LocallyIntegrableOn f Set.univ μ ↔ LocallyIntegrable f μ

theorem MeasureTheory.LocallyIntegrable.locallyIntegrableOn {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} (hf : LocallyIntegrable f μ) (s : Set X) : LocallyIntegrableOn f s μ

theorem MeasureTheory.Integrable.locallyIntegrable {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} (hf : Integrable f μ) : LocallyIntegrable f μ

theorem MeasureTheory.LocallyIntegrable.mono_enorm {X : Type u_1} {ε : Type u_3} {ε' : Type u_4} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] [TopologicalSpace ε'] [ContinuousENorm ε'] {f : X → ε} {μ : Measure X} (hf : LocallyIntegrable f μ) {g : X → ε'} (hg : AEStronglyMeasurable g μ) (h : ∀ᵐ (x : X) ∂μ, ‖g x‖ₑ ≤ ‖f x‖ₑ) : LocallyIntegrable g μ

theorem MeasureTheory.LocallyIntegrable.mono {X : Type u_1} {E : Type u_6} {F : Type u_7} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] [NormedAddCommGroup F] {μ : Measure X} {f : X → E} (hf : LocallyIntegrable f μ) {g : X → F} (hg : AEStronglyMeasurable g μ) (h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖) : LocallyIntegrable g μ

theorem MeasureTheory.locallyIntegrableOn_of_locallyIntegrable_restrict {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} {s : Set X} [OpensMeasurableSpace X] (hf : LocallyIntegrable f (μ.restrict s)) : LocallyIntegrableOn f s μ

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} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} {s : Set X} [OpensMeasurableSpace X] (hs : IsClosed s) : LocallyIntegrableOn f s μ ↔ LocallyIntegrable f (μ.restrict s)

If s is closed, being locally integrable on s w.r.t. μ 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} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} [TopologicalSpace.PseudoMetrizableSpace ε] {k : Set X} (hf : LocallyIntegrable f μ) (hk : IsCompact k) : IntegrableOn f 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} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} [TopologicalSpace.PseudoMetrizableSpace ε] (hf : LocallyIntegrable f μ) {k : Set X} (hk : IsCompact k) : ∃ (u : Set X), IsOpen u ∧ k ⊆ u ∧ 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} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} [TopologicalSpace.PseudoMetrizableSpace ε] [LocallyCompactSpace X] : LocallyIntegrable f μ ↔ ∀ (k : Set X), IsCompact k → IntegrableOn f k μ

theorem MeasureTheory.LocallyIntegrable.aestronglyMeasurable {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} [TopologicalSpace.PseudoMetrizableSpace ε] [SecondCountableTopology X] (hf : LocallyIntegrable f μ) : AEStronglyMeasurable f μ

theorem MeasureTheory.LocallyIntegrable.exists_nat_integrableOn {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} [SecondCountableTopology X] (hf : LocallyIntegrable f μ) : ∃ (u : ℕ → Set X), (∀ (n : ℕ), IsOpen (u n)) ∧ ⋃ (n : ℕ), u n = Set.univ ∧ ∀ (n : ℕ), IntegrableOn f (u n) μ

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.MemLp.locallyIntegrable {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} [IsLocallyFiniteMeasure μ] {p : ENNReal} (hf : MemLp f p μ) (hp : 1 ≤ p) : LocallyIntegrable f μ

theorem MeasureTheory.locallyIntegrable_const_enorm {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {μ : Measure X} [IsLocallyFiniteMeasure μ] {c : ε} (hc : ‖c‖ₑ ≠ ⊤) : LocallyIntegrable (fun (x : X) => c) μ

theorem MeasureTheory.locallyIntegrable_const {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : Measure X} [IsLocallyFiniteMeasure μ] (c : E) : LocallyIntegrable (fun (x : X) => c) μ

theorem MeasureTheory.locallyIntegrableOn_const_enorm {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {μ : Measure X} {s : Set X} [IsLocallyFiniteMeasure μ] {c : ε} (hc : ‖c‖ₑ ≠ ⊤) : LocallyIntegrableOn (fun (x : X) => c) s μ

theorem MeasureTheory.locallyIntegrableOn_const {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : Measure X} {s : Set X} [IsLocallyFiniteMeasure μ] (c : E) : LocallyIntegrableOn (fun (x : X) => c) s μ

theorem MeasureTheory.locallyIntegrable_zero {X : Type u_1} {ε'' : Type u_5} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε''] [ESeminormedAddMonoid ε''] {μ : Measure X} : LocallyIntegrable (fun (x : X) => 0) μ

theorem MeasureTheory.locallyIntegrableOn_zero {X : Type u_1} {ε'' : Type u_5} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε''] [ESeminormedAddMonoid ε''] {μ : Measure X} {s : Set X} : LocallyIntegrableOn (fun (x : X) => 0) s μ

theorem MeasureTheory.LocallyIntegrable.indicator {X : Type u_1} {ε'' : Type u_5} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε''] [ESeminormedAddMonoid ε''] {μ : Measure X} {f : X → ε''} (hf : LocallyIntegrable f μ) {s : Set X} (hs : MeasurableSet s) : LocallyIntegrable (s.indicator f) μ

theorem MeasureTheory.locallyIntegrable_map_homeomorph {X : Type u_1} {Y : Type u_2} {ε'' : Type u_5} [MeasurableSpace X] [TopologicalSpace X] [MeasurableSpace Y] [TopologicalSpace Y] [TopologicalSpace ε''] [ESeminormedAddMonoid ε''] [BorelSpace X] [BorelSpace Y] (e : X ≃ₜ Y) {f : Y → ε''} {μ : Measure X} : LocallyIntegrable f (Measure.map (⇑e) μ) ↔ LocallyIntegrable (f ∘ ⇑e) μ

theorem MeasureTheory.LocallyIntegrable.add {X : Type u_1} {ε'' : Type u_5} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε''] [ESeminormedAddMonoid ε''] {μ : Measure X} [ContinuousAdd ε''] {f g : X → ε''} (hf : LocallyIntegrable f μ) (hg : LocallyIntegrable g μ) : LocallyIntegrable (f + g) μ

theorem MeasureTheory.LocallyIntegrable.sub {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : Measure X} {f g : X → E} (hf : LocallyIntegrable f μ) (hg : LocallyIntegrable g μ) : LocallyIntegrable (f - g) μ

theorem MeasureTheory.LocallyIntegrable.neg {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : Measure X} {f : X → E} (hf : LocallyIntegrable f μ) : LocallyIntegrable (-f) μ

theorem MeasureTheory.LocallyIntegrable.smul {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : Measure X} {f : X → E} {𝕜 : Type u_9} [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 E] [IsBoundedSMul 𝕜 E] (hf : LocallyIntegrable f μ) (c : 𝕜) : LocallyIntegrable (c • f) μ

theorem MeasureTheory.locallyIntegrable_finset_sum' {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] {μ : Measure X} {ε''' : Type u_9} [TopologicalSpace ε'''] [ESeminormedAddCommMonoid ε'''] [ContinuousAdd ε'''] {ι : Type u_10} (s : Finset ι) {f : ι → X → ε'''} (hf : ∀ i ∈ s, LocallyIntegrable (f i) μ) : LocallyIntegrable (∑ i ∈ s, f i) μ

theorem MeasureTheory.locallyIntegrable_finset_sum {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] {μ : Measure X} {ε''' : Type u_9} [TopologicalSpace ε'''] [ESeminormedAddCommMonoid ε'''] [ContinuousAdd ε'''] {ι : Type u_10} (s : Finset ι) {f : ι → X → ε'''} (hf : ∀ i ∈ s, LocallyIntegrable (f i) μ) : LocallyIntegrable (fun (a : X) => ∑ i ∈ s, f i a) μ

theorem MeasureTheory.LocallyIntegrable.integrable_smul_left_of_hasCompactSupport {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : Measure X} {𝕜 : Type u_9} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [OpensMeasurableSpace X] [T2Space X] {f : X → E} (hf : LocallyIntegrable f μ) {g : X → 𝕜} (hg : Continuous g) (h'g : HasCompactSupport g) : Integrable (fun (x : 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_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : Measure X} {𝕜 : Type u_9} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [OpensMeasurableSpace X] [T2Space X] {f : X → 𝕜} (hf : LocallyIntegrable f μ) {g : X → E} (hg : Continuous g) (h'g : HasCompactSupport g) : Integrable (fun (x : X) => f x • g x) μ

If f is locally integrable and g is continuous with compact support, then f • g is integrable.

theorem MeasureTheory.integrable_iff_integrableAtFilter_cocompact {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} [TopologicalSpace.PseudoMetrizableSpace ε] : Integrable f μ ↔ IntegrableAtFilter f (Filter.cocompact X) μ ∧ LocallyIntegrable f μ

theorem MeasureTheory.integrable_iff_integrableAtFilter_atBot_atTop {X : Type u_1} {ε'' : Type u_5} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε''] [ESeminormedAddMonoid ε''] {μ : Measure X} [TopologicalSpace.PseudoMetrizableSpace ε''] {f : X → ε''} [LinearOrder X] [CompactIccSpace X] : Integrable f μ ↔ (IntegrableAtFilter f Filter.atBot μ ∧ IntegrableAtFilter f Filter.atTop μ) ∧ LocallyIntegrable f μ

theorem MeasureTheory.integrable_iff_integrableAtFilter_atBot {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} [TopologicalSpace.PseudoMetrizableSpace ε] [LinearOrder X] [OrderTop X] [CompactIccSpace X] : Integrable f μ ↔ IntegrableAtFilter f Filter.atBot μ ∧ LocallyIntegrable f μ

theorem MeasureTheory.integrable_iff_integrableAtFilter_atTop {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} [TopologicalSpace.PseudoMetrizableSpace ε] [LinearOrder X] [OrderBot X] [CompactIccSpace X] : Integrable f μ ↔ IntegrableAtFilter f Filter.atTop μ ∧ LocallyIntegrable f μ

theorem MeasureTheory.integrableOn_Iic_iff_integrableAtFilter_atBot {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} [TopologicalSpace.PseudoMetrizableSpace ε] {a : X} [LinearOrder X] [CompactIccSpace X] : IntegrableOn f (Set.Iic a) μ ↔ IntegrableAtFilter f Filter.atBot μ ∧ LocallyIntegrableOn f (Set.Iic a) μ

theorem MeasureTheory.integrableOn_Ici_iff_integrableAtFilter_atTop {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} [TopologicalSpace.PseudoMetrizableSpace ε] {a : X} [LinearOrder X] [CompactIccSpace X] : IntegrableOn f (Set.Ici a) μ ↔ IntegrableAtFilter f Filter.atTop μ ∧ LocallyIntegrableOn f (Set.Ici a) μ

theorem MeasureTheory.integrableOn_Iio_iff_integrableAtFilter_atBot_nhdsWithin {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} [TopologicalSpace.PseudoMetrizableSpace ε] {a : X} [LinearOrder X] [CompactIccSpace X] [NoMinOrder X] [OrderTopology X] : IntegrableOn f (Set.Iio a) μ ↔ IntegrableAtFilter f Filter.atBot μ ∧ IntegrableAtFilter f (nhdsWithin a (Set.Iio a)) μ ∧ LocallyIntegrableOn f (Set.Iio a) μ

theorem MeasureTheory.integrableOn_Ioi_iff_integrableAtFilter_atTop_nhdsWithin {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : Measure X} [TopologicalSpace.PseudoMetrizableSpace ε] {a : X} [LinearOrder X] [CompactIccSpace X] [NoMaxOrder X] [OrderTopology X] : IntegrableOn f (Set.Ioi a) μ ↔ IntegrableAtFilter f Filter.atTop μ ∧ IntegrableAtFilter f (nhdsWithin a (Set.Ioi a)) μ ∧ LocallyIntegrableOn f (Set.Ioi a) μ

theorem Continuous.locallyIntegrable {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {f : X → E} [MeasureTheory.IsLocallyFiniteMeasure μ] [SecondCountableTopologyEither X E] (hf : Continuous f) : MeasureTheory.LocallyIntegrable 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_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {K : Set X} {f : X → E} [MeasureTheory.IsLocallyFiniteMeasure μ] [SecondCountableTopologyEither X E] (hf : ContinuousOn f K) (hK : MeasurableSet K) : MeasureTheory.LocallyIntegrableOn f 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_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {K : Set X} {f : X → E} [MeasureTheory.IsFiniteMeasureOnCompacts μ] (hK : IsCompact K) (h'K : MeasurableSet K) (hf : ContinuousOn f K) : MeasureTheory.IntegrableOn 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_compact {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {K : Set X} {f : X → E} [MeasureTheory.IsFiniteMeasureOnCompacts μ] [T2Space X] (hK : IsCompact K) (hf : ContinuousOn f K) : MeasureTheory.IntegrableOn f K μ

theorem ContinuousOn.integrableOn_Icc {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {f : X → E} {a b : X} [MeasureTheory.IsFiniteMeasureOnCompacts μ] [Preorder X] [CompactIccSpace X] [T2Space 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_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {f : X → E} {a b : X} [MeasureTheory.IsFiniteMeasureOnCompacts μ] [Preorder X] [CompactIccSpace X] [T2Space X] (hf : Continuous f) : MeasureTheory.IntegrableOn f (Set.Icc a b) μ

theorem Continuous.integrableOn_Ioc {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {f : X → E} {a b : X} [MeasureTheory.IsFiniteMeasureOnCompacts μ] [Preorder X] [CompactIccSpace X] [T2Space X] (hf : Continuous f) : MeasureTheory.IntegrableOn f (Set.Ioc a b) μ

theorem ContinuousOn.integrableOn_uIcc {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {f : X → E} {a b : X} [MeasureTheory.IsFiniteMeasureOnCompacts μ] [LinearOrder X] [CompactIccSpace X] [T2Space 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_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {f : X → E} {a b : X} [MeasureTheory.IsFiniteMeasureOnCompacts μ] [LinearOrder X] [CompactIccSpace X] [T2Space X] (hf : Continuous f) : MeasureTheory.IntegrableOn f (Set.uIcc a b) μ

theorem Continuous.integrableOn_uIoc {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {f : X → E} {a b : X} [MeasureTheory.IsFiniteMeasureOnCompacts μ] [LinearOrder X] [CompactIccSpace X] [T2Space X] (hf : Continuous f) : MeasureTheory.IntegrableOn f (Set.uIoc a b) μ

theorem Continuous.integrable_of_hasCompactSupport {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {f : X → E} [MeasureTheory.IsFiniteMeasureOnCompacts μ] (hf : Continuous f) (hcf : HasCompactSupport f) : MeasureTheory.Integrable f μ

A continuous function with compact support is integrable on the whole space.

theorem MonotoneOn.memLp_top {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [ConditionallyCompleteLinearOrder X] [ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E] {f : X → E} (hmono : MonotoneOn f s) {a b : X} (ha : IsLeast s a) (hb : IsGreatest s b) (h's : MeasurableSet s) : MeasureTheory.MemLp f ⊤ (μ.restrict s)

theorem MonotoneOn.memLp_of_measure_ne_top {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [ConditionallyCompleteLinearOrder X] [ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E] {p : ENNReal} {f : X → E} (hmono : MonotoneOn f s) {a b : X} (ha : IsLeast s a) (hb : IsGreatest s b) (hs : μ s ≠ ⊤) (h's : MeasurableSet s) : MeasureTheory.MemLp f p (μ.restrict s)

theorem MonotoneOn.memLp_isCompact {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [ConditionallyCompleteLinearOrder X] [ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E] {p : ENNReal} {f : X → E} [MeasureTheory.IsFiniteMeasureOnCompacts μ] (hs : IsCompact s) (hmono : MonotoneOn f s) : MeasureTheory.MemLp f p (μ.restrict s)

theorem AntitoneOn.memLp_top {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [ConditionallyCompleteLinearOrder X] [ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E] {f : X → E} (hanti : AntitoneOn f s) {a b : X} (ha : IsLeast s a) (hb : IsGreatest s b) (h's : MeasurableSet s) : MeasureTheory.MemLp f ⊤ (μ.restrict s)

theorem AntitoneOn.memLp_of_measure_ne_top {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [ConditionallyCompleteLinearOrder X] [ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E] {p : ENNReal} {f : X → E} (hanti : AntitoneOn f s) {a b : X} (ha : IsLeast s a) (hb : IsGreatest s b) (hs : μ s ≠ ⊤) (h's : MeasurableSet s) : MeasureTheory.MemLp f p (μ.restrict s)

theorem AntitoneOn.memLp_isCompact {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [ConditionallyCompleteLinearOrder X] [ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E] {p : ENNReal} {f : X → E} [MeasureTheory.IsFiniteMeasureOnCompacts μ] (hs : IsCompact s) (hanti : AntitoneOn f s) : MeasureTheory.MemLp f p (μ.restrict s)

theorem MonotoneOn.integrableOn_of_measure_ne_top {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [ConditionallyCompleteLinearOrder X] [ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E] {f : X → E} (hmono : MonotoneOn f s) {a b : X} (ha : IsLeast s a) (hb : IsGreatest s b) (hs : μ s ≠ ⊤) (h's : MeasurableSet s) : MeasureTheory.IntegrableOn f s μ

theorem MonotoneOn.integrableOn_isCompact {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [ConditionallyCompleteLinearOrder X] [ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E] {f : X → E} [MeasureTheory.IsFiniteMeasureOnCompacts μ] (hs : IsCompact s) (hmono : MonotoneOn f s) : MeasureTheory.IntegrableOn f s μ

theorem AntitoneOn.integrableOn_of_measure_ne_top {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [ConditionallyCompleteLinearOrder X] [ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E] {f : X → E} (hanti : AntitoneOn f s) {a b : X} (ha : IsLeast s a) (hb : IsGreatest s b) (hs : μ s ≠ ⊤) (h's : MeasurableSet s) : MeasureTheory.IntegrableOn f s μ

theorem AntitoneOn.integrableOn_isCompact {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [ConditionallyCompleteLinearOrder X] [ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E] {f : X → E} [MeasureTheory.IsFiniteMeasureOnCompacts μ] (hs : IsCompact s) (hanti : AntitoneOn f s) : MeasureTheory.IntegrableOn f s μ

theorem Monotone.locallyIntegrable {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [BorelSpace X] [ConditionallyCompleteLinearOrder X] [ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E] {f : X → E} [MeasureTheory.IsLocallyFiniteMeasure μ] (hmono : Monotone f) : MeasureTheory.LocallyIntegrable f μ

theorem Antitone.locallyIntegrable {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [BorelSpace X] [ConditionallyCompleteLinearOrder X] [ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E] {f : X → E} [MeasureTheory.IsLocallyFiniteMeasure μ] (hanti : Antitone f) : MeasureTheory.LocallyIntegrable f μ

theorem MeasureTheory.IntegrableOn.mul_continuousOn_of_subset {X : Type u_1} {R : Type u_8} [MeasurableSpace X] [TopologicalSpace X] {μ : Measure X} [OpensMeasurableSpace X] {A K : Set X} [NormedRing R] [SecondCountableTopologyEither X R] {g g' : X → R} (hg : IntegrableOn g A μ) (hg' : ContinuousOn g' K) (hA : MeasurableSet A) (hK : IsCompact K) (hAK : A ⊆ K) : IntegrableOn (fun (x : X) => g x * g' x) A μ

theorem MeasureTheory.IntegrableOn.mul_continuousOn {X : Type u_1} {R : Type u_8} [MeasurableSpace X] [TopologicalSpace X] {μ : Measure X} [OpensMeasurableSpace X] {K : Set X} [NormedRing R] [SecondCountableTopologyEither X R] {g g' : X → R} [T2Space X] (hg : IntegrableOn g K μ) (hg' : ContinuousOn g' K) (hK : IsCompact K) : IntegrableOn (fun (x : X) => g x * g' x) K μ

theorem MeasureTheory.IntegrableOn.continuousOn_mul_of_subset {X : Type u_1} {R : Type u_8} [MeasurableSpace X] [TopologicalSpace X] {μ : Measure X} [OpensMeasurableSpace X] {A K : Set X} [NormedRing R] [SecondCountableTopologyEither X R] {g g' : X → R} (hg : ContinuousOn g K) (hg' : IntegrableOn g' A μ) (hK : IsCompact K) (hA : MeasurableSet A) (hAK : A ⊆ K) : IntegrableOn (fun (x : X) => g x * g' x) A μ

theorem MeasureTheory.IntegrableOn.continuousOn_mul {X : Type u_1} {R : Type u_8} [MeasurableSpace X] [TopologicalSpace X] {μ : Measure X} [OpensMeasurableSpace X] {K : Set X} [NormedRing R] [SecondCountableTopologyEither X R] {g g' : X → R} [T2Space X] (hg : ContinuousOn g K) (hg' : IntegrableOn g' K μ) (hK : IsCompact K) : IntegrableOn (fun (x : X) => g x * g' x) K μ

theorem MeasureTheory.IntegrableOn.continuousOn_smul_of_subset {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : Measure X} [OpensMeasurableSpace X] {A K : Set X} {𝕜 : Type u_9} [NormedRing 𝕜] [Module 𝕜 E] [NormSMulClass 𝕜 E] [SecondCountableTopologyEither X 𝕜] {f : X → 𝕜} (hf : ContinuousOn f K) {g : X → E} (hg : IntegrableOn g A μ) (hK : IsCompact K) (hA : MeasurableSet A) (hAK : A ⊆ K) : IntegrableOn (fun (x : X) => f x • g x) A μ

theorem MeasureTheory.IntegrableOn.continuousOn_smul {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : Measure X} [OpensMeasurableSpace X] {K : Set X} {𝕜 : Type u_9} [NormedRing 𝕜] [Module 𝕜 E] [NormSMulClass 𝕜 E] [T2Space X] [SecondCountableTopologyEither X 𝕜] {g : X → E} (hg : IntegrableOn g K μ) {f : X → 𝕜} (hf : ContinuousOn f K) (hK : IsCompact K) : IntegrableOn (fun (x : X) => f x • g x) K μ

theorem MeasureTheory.IntegrableOn.smul_continuousOn_of_subset {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : Measure X} [OpensMeasurableSpace X] {A K : Set X} {𝕜 : Type u_9} [NormedRing 𝕜] [Module 𝕜 E] [NormSMulClass 𝕜 E] [SecondCountableTopologyEither X E] {f : X → 𝕜} (hf : IntegrableOn f A μ) {g : X → E} (hg : ContinuousOn g K) (hA : MeasurableSet A) (hK : IsCompact K) (hAK : A ⊆ K) : IntegrableOn (fun (x : X) => f x • g x) A μ

theorem MeasureTheory.IntegrableOn.smul_continuousOn {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : Measure X} [OpensMeasurableSpace X] {K : Set X} {𝕜 : Type u_9} [NormedRing 𝕜] [Module 𝕜 E] [NormSMulClass 𝕜 E] [T2Space X] [SecondCountableTopologyEither X E] {f : X → 𝕜} (hf : IntegrableOn f K μ) {g : X → E} (hg : ContinuousOn g K) (hK : IsCompact K) : IntegrableOn (fun (x : X) => f x • g x) K μ

theorem MeasureTheory.LocallyIntegrableOn.continuousOn_mul {X : Type u_1} {R : Type u_8} [MeasurableSpace X] [TopologicalSpace X] {μ : Measure X} [OpensMeasurableSpace X] [LocallyCompactSpace X] [T2Space X] [NormedRing R] [SecondCountableTopologyEither X R] {f g : X → R} {s : Set X} (hf : LocallyIntegrableOn f s μ) (hg : ContinuousOn g s) (hs : IsLocallyClosed s) : LocallyIntegrableOn (fun (x : X) => g x * f x) s μ

theorem MeasureTheory.LocallyIntegrableOn.mul_continuousOn {X : Type u_1} {R : Type u_8} [MeasurableSpace X] [TopologicalSpace X] {μ : Measure X} [OpensMeasurableSpace X] [LocallyCompactSpace X] [T2Space X] [NormedRing R] [SecondCountableTopologyEither X R] {f g : X → R} {s : Set X} (hf : LocallyIntegrableOn f s μ) (hg : ContinuousOn g s) (hs : IsLocallyClosed s) : LocallyIntegrableOn (fun (x : X) => f x * g x) s μ

theorem MeasureTheory.LocallyIntegrableOn.continuousOn_smul {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : Measure X} [OpensMeasurableSpace X] [LocallyCompactSpace X] [T2Space X] {𝕜 : Type u_9} [NormedRing 𝕜] [SecondCountableTopologyEither X 𝕜] [Module 𝕜 E] [NormSMulClass 𝕜 E] {f : X → E} {g : X → 𝕜} {s : Set X} (hs : IsLocallyClosed s) (hf : LocallyIntegrableOn f s μ) (hg : ContinuousOn g s) : LocallyIntegrableOn (fun (x : X) => g x • f x) s μ

theorem MeasureTheory.LocallyIntegrableOn.smul_continuousOn {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : Measure X} [OpensMeasurableSpace X] [LocallyCompactSpace X] [T2Space X] {𝕜 : Type u_9} [NormedRing 𝕜] [SecondCountableTopologyEither X E] [Module 𝕜 E] [NormSMulClass 𝕜 E] {f : X → 𝕜} {g : X → E} {s : Set X} (hs : IsLocallyClosed s) (hf : LocallyIntegrableOn f s μ) (hg : ContinuousOn g s) : LocallyIntegrableOn (fun (x : X) => f x • g x) s μ