Documentation

Mathlib.MeasureTheory.Function.LocallyIntegrable

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 #

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
Instances For
    theorem MeasureTheory.LocallyIntegrableOn.mono {X : Type u_1} {E : Type u_3} {F : Type u_4} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] [NormedAddCommGroup F] {f : XE} {μ : MeasureTheory.Measure X} {s : Set X} (hf : MeasureTheory.LocallyIntegrableOn f s μ) {g : XF} (hg : MeasureTheory.AEStronglyMeasurable g μ) (h : ∀ᵐ (x : X) ∂μ, g x f x) :

    If a function is locally integrable on a compact set, then it is integrable on that set.

    theorem MeasureTheory.LocallyIntegrableOn.exists_countable_integrableOn {X : Type u_1} {E : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {f : XE} {μ : MeasureTheory.Measure X} {s : Set X} [SecondCountableTopology X] (hf : MeasureTheory.LocallyIntegrableOn f s μ) :
    ∃ (T : Set (Set X)), Set.Countable T (uT, IsOpen u) s ⋃ u ∈ T, u uT, MeasureTheory.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} {E : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {f : XE} {μ : MeasureTheory.Measure X} {s : Set X} [SecondCountableTopology X] (hf : MeasureTheory.LocallyIntegrableOn f s μ) :
    ∃ (u : Set X), (∀ (n : ), IsOpen (u n)) s ⋃ (n : ), u n ∀ (n : ), MeasureTheory.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.

    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.

    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
    Instances For
      theorem MeasureTheory.LocallyIntegrable.mono {X : Type u_1} {E : Type u_3} {F : Type u_4} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] [NormedAddCommGroup F] {f : XE} {μ : MeasureTheory.Measure X} (hf : MeasureTheory.LocallyIntegrable f μ) {g : XF} (hg : MeasureTheory.AEStronglyMeasurable g μ) (h : ∀ᵐ (x : X) ∂μ, g x f x) :

      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.)

      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.

      If a function is locally integrable, then it is integrable on any compact set.

      If a function is locally integrable, then it is integrable on an open neighborhood of any compact set.

      theorem MeasureTheory.LocallyIntegrable.exists_nat_integrableOn {X : Type u_1} {E : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {f : XE} {μ : MeasureTheory.Measure X} [SecondCountableTopology X] (hf : MeasureTheory.LocallyIntegrable f μ) :
      ∃ (u : Set X), (∀ (n : ), IsOpen (u n)) ⋃ (n : ), u n = Set.univ ∀ (n : ), MeasureTheory.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.locallyIntegrable_finset_sum' {X : Type u_1} {E : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {ι : Type u_6} (s : Finset ι) {f : ιXE} (hf : is, 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_6} (s : Finset ι) {f : ιXE} (hf : is, MeasureTheory.LocallyIntegrable (f i) μ) :
      MeasureTheory.LocallyIntegrable (fun (a : X) => Finset.sum s fun (i : ι) => f i a) μ

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

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

      A continuous function f is locally integrable with respect to any locally finite measure.

      A function f continuous on a set K is locally integrable on this set with respect to any locally finite measure.

      A function f continuous on a compact set K is integrable on this set with respect to any locally finite measure.

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

      theorem MeasureTheory.IntegrableOn.mul_continuousOn_of_subset {X : Type u_1} {R : Type u_5} [MeasurableSpace X] [TopologicalSpace X] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {A : Set X} {K : Set X} [NormedRing R] [SecondCountableTopologyEither X R] {g : XR} {g' : XR} (hg : MeasureTheory.IntegrableOn g A μ) (hg' : ContinuousOn g' K) (hA : MeasurableSet A) (hK : IsCompact K) (hAK : A K) :
      MeasureTheory.IntegrableOn (fun (x : X) => g x * g' x) A μ
      theorem MeasureTheory.IntegrableOn.mul_continuousOn {X : Type u_1} {R : Type u_5} [MeasurableSpace X] [TopologicalSpace X] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {K : Set X} [NormedRing R] [SecondCountableTopologyEither X R] {g : XR} {g' : XR} [T2Space X] (hg : MeasureTheory.IntegrableOn g K μ) (hg' : ContinuousOn g' K) (hK : IsCompact K) :
      MeasureTheory.IntegrableOn (fun (x : X) => g x * g' x) K μ
      theorem MeasureTheory.IntegrableOn.continuousOn_mul_of_subset {X : Type u_1} {R : Type u_5} [MeasurableSpace X] [TopologicalSpace X] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {A : Set X} {K : Set X} [NormedRing R] [SecondCountableTopologyEither X R] {g : XR} {g' : XR} (hg : ContinuousOn g K) (hg' : MeasureTheory.IntegrableOn g' A μ) (hK : IsCompact K) (hA : MeasurableSet A) (hAK : A K) :
      MeasureTheory.IntegrableOn (fun (x : X) => g x * g' x) A μ
      theorem MeasureTheory.IntegrableOn.continuousOn_mul {X : Type u_1} {R : Type u_5} [MeasurableSpace X] [TopologicalSpace X] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {K : Set X} [NormedRing R] [SecondCountableTopologyEither X R] {g : XR} {g' : XR} [T2Space X] (hg : ContinuousOn g K) (hg' : MeasureTheory.IntegrableOn g' K μ) (hK : IsCompact K) :
      MeasureTheory.IntegrableOn (fun (x : 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_6} [NormedField 𝕜] [NormedSpace 𝕜 E] [T2Space X] [SecondCountableTopologyEither X 𝕜] {g : XE} (hg : MeasureTheory.IntegrableOn g K μ) {f : X𝕜} (hf : ContinuousOn f K) (hK : IsCompact K) :
      MeasureTheory.IntegrableOn (fun (x : 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_6} [NormedField 𝕜] [NormedSpace 𝕜 E] [T2Space X] [SecondCountableTopologyEither X E] {f : X𝕜} (hf : MeasureTheory.IntegrableOn f K μ) {g : XE} (hg : ContinuousOn g K) (hK : IsCompact K) :
      MeasureTheory.IntegrableOn (fun (x : X) => f x g x) K μ
      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_6} [NormedField 𝕜] [SecondCountableTopologyEither X 𝕜] [NormedSpace 𝕜 E] {f : XE} {g : X𝕜} {s : Set X} (hs : IsOpen s) (hf : MeasureTheory.LocallyIntegrableOn f s μ) (hg : ContinuousOn g s) :
      MeasureTheory.LocallyIntegrableOn (fun (x : 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_6} [NormedField 𝕜] [SecondCountableTopologyEither X E] [NormedSpace 𝕜 E] {f : X𝕜} {g : XE} {s : Set X} (hs : IsOpen s) (hf : MeasureTheory.LocallyIntegrableOn f s μ) (hg : ContinuousOn g s) :
      MeasureTheory.LocallyIntegrableOn (fun (x : X) => f x g x) s μ