Local integrability

Local integrability on an open set is equivalent to local integrability on every open subdomain whose closure is compact and contained in the original set. This form is useful when a proof can be localized to relatively compact subdomains.

For a right-translation-invariant measure on an additive group with continuous addition, local integrability is preserved by translating a function onto any set whose translate stays inside the original domain.

A function locally integrable on a null-measurable set s, vanishing almost everywhere on s off a null-measurable compact K ⊆ s, is integrable on the whole space after extension by zero. This is the step that turns a local hypothesis plus compact support into a global one. Both sets are asked to be null-measurable explicitly because nothing here ties the topology on X to its measurable space -- there is no OpensMeasurableSpace or BorelSpace assumption, so neither compactness nor closedness of K carries any measurability with it. (Absent a separation axiom K need not even be closed, but that is the lesser obstacle.)

Main declarations

• MeasureTheory.LocallyIntegrableOn.comp_add_right_of_mapsTo: translation onto a smaller set preserves local integrability.
• TauCeti.locallyIntegrableOn_iff_forall_isCompact_closure: characterization by relatively compact open subdomains.
• MeasureTheory.LocallyIntegrableOn.integrable_indicator_of_isCompact: integrability of the extension by zero of a locally integrable function supported in a null-measurable compact subset.

Attribution

The characterization uses Mathlib's exists_open_between_and_isCompact_closure to find relatively compact open neighborhoods of individual points. Extension by zero rests on Mathlib's LocallyIntegrableOn.integrableOn_compact_subset, which gives integrability on the compact support.

theorem MeasureTheory.LocallyIntegrableOn.comp_add_right_of_mapsTo {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [AddGroup E] [TopologicalSpace E] [ContinuousAdd E] [BorelSpace E] [TopologicalSpace F] [ContinuousENorm F] {mu : Measure E} [mu.IsAddRightInvariant] {Omega V : Set E} {u : E → F} {h : E} (hu : LocallyIntegrableOn u Omega mu) (hVO : Set.MapsTo (fun (x : E) => x + h) V Omega) : LocallyIntegrableOn (fun (x : E) => u (x + h)) V mu

Local integrability is preserved by a translation whose image stays in the original domain.

theorem TauCeti.locallyIntegrableOn_iff_forall_isCompact_closure {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] {μ : MeasureTheory.Measure X} {ε : Type u_2} [TopologicalSpace ε] [ContinuousENorm ε] [LocallyCompactSpace X] [RegularSpace X] {f : X → ε} {Ω : TopologicalSpace.Opens X} : MeasureTheory.LocallyIntegrableOn f (↑Ω) μ ↔ ∀ (V : TopologicalSpace.Opens X), IsCompact (closure ↑V) → closure ↑V ⊆ ↑Ω → MeasureTheory.LocallyIntegrableOn f (↑V) μ

A function is locally integrable on an open set exactly when it is locally integrable on every open subdomain with compact closure contained in that set.

theorem MeasureTheory.LocallyIntegrableOn.integrable_indicator_of_isCompact {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] {μ : Measure X} {ε : Type u_2} [TopologicalSpace ε] [ESeminormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε] {f : X → ε} {s K : Set X} (hloc : LocallyIntegrableOn f s μ) (hs : NullMeasurableSet s μ) (hK : IsCompact K) (hKmeas : NullMeasurableSet K μ) (hKs : K ⊆ s) (hf : ∀ᵐ (x : X) ∂μ.restrict s, x ∉ K → f x = 0) : Integrable (s.indicator f) μ

A function locally integrable on a null-measurable set s and vanishing almost everywhere on s off a null-measurable compact K ⊆ s is, after extension by zero, integrable on the whole space.

K carries its own null-measurability hypothesis rather than inheriting one from compactness: no assumption here relates the topology on X to its measurable space, so a compact -- or even closed -- set need not be measurable at all.