# 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} {E : Type u_3} [] [] (f : XE) (s : Set X) (μ : ) :

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
• = xs,
Instances For
theorem MeasureTheory.LocallyIntegrableOn.mono_set {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {s : Set X} (hf : ) {t : Set X} (hst : t s) :
theorem MeasureTheory.LocallyIntegrableOn.norm {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {s : Set X} (hf : ) :
MeasureTheory.LocallyIntegrableOn (fun (x : X) => f x) s μ
theorem MeasureTheory.LocallyIntegrableOn.mono {X : Type u_1} {E : Type u_3} {F : Type u_4} [] [] {f : XE} {μ : } {s : Set X} (hf : ) {g : XF} (hg : ) (h : ∀ᵐ (x : X) ∂μ, g x f x) :
theorem MeasureTheory.IntegrableOn.locallyIntegrableOn {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {s : Set X} (hf : ) :
theorem MeasureTheory.LocallyIntegrableOn.integrableOn_isCompact {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {s : Set X} (hf : ) (hs : ) :

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} [] [] {f : XE} {μ : } {s : Set X} (hf : ) {t : Set X} (hst : t s) (ht : ) :
theorem MeasureTheory.LocallyIntegrableOn.exists_countable_integrableOn {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {s : Set X} (hf : ) :
∃ (T : Set (Set X)), T.Countable (∀ uT, ) s uT, 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} [] [] {f : XE} {μ : } {s : Set X} (hf : ) :
∃ (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.

theorem MeasureTheory.LocallyIntegrableOn.aestronglyMeasurable {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {s : Set X} (hf : ) :
theorem MeasureTheory.locallyIntegrableOn_iff {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {s : Set X} [] (hs : ) :
ks,

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} [] [] {f : XE} {g : XE} {μ : } {s : Set X} (hf : ) (hg : ) :
theorem MeasureTheory.LocallyIntegrableOn.sub {X : Type u_1} {E : Type u_3} [] [] {f : XE} {g : XE} {μ : } {s : Set X} (hf : ) (hg : ) :
theorem MeasureTheory.LocallyIntegrableOn.neg {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {s : Set X} (hf : ) :
def MeasureTheory.LocallyIntegrable {X : Type u_1} {E : Type u_3} [] [] (f : XE) (μ : ) :

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
• = ∀ (x : X),
Instances For
theorem MeasureTheory.locallyIntegrable_comap {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {s : Set X} (hs : ) :
MeasureTheory.LocallyIntegrable (fun (x : s) => f x) (MeasureTheory.Measure.comap Subtype.val μ)
theorem MeasureTheory.locallyIntegrableOn_univ {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } :
theorem MeasureTheory.LocallyIntegrable.locallyIntegrableOn {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } (hf : ) (s : Set X) :
theorem MeasureTheory.Integrable.locallyIntegrable {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } (hf : ) :
theorem MeasureTheory.LocallyIntegrable.mono {X : Type u_1} {E : Type u_3} {F : Type u_4} [] [] {f : XE} {μ : } (hf : ) {g : XF} (hg : ) (h : ∀ᵐ (x : X) ∂μ, g x f x) :
theorem MeasureTheory.locallyIntegrableOn_of_locallyIntegrable_restrict {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {s : Set X} (hf : MeasureTheory.LocallyIntegrable f (μ.restrict 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} {E : Type u_3} [] [] {f : XE} {μ : } {s : Set X} (hs : ) :

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} [] [] {f : XE} {μ : } {k : Set X} (hf : ) (hk : ) :

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} [] [] {f : XE} {μ : } (hf : ) {k : Set X} (hk : ) :
∃ (u : Set X), k 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} [] [] {f : XE} {μ : } :
∀ (k : Set X),
theorem MeasureTheory.LocallyIntegrable.aestronglyMeasurable {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } (hf : ) :
theorem MeasureTheory.LocallyIntegrable.exists_nat_integrableOn {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } (hf : ) :
∃ (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.Memℒp.locallyIntegrable {X : Type u_1} {E : Type u_3} [] [] {μ : } {f : XE} {p : ENNReal} (hf : ) (hp : 1 p) :
theorem MeasureTheory.locallyIntegrable_const {X : Type u_1} {E : Type u_3} [] [] {μ : } (c : E) :
MeasureTheory.LocallyIntegrable (fun (x : X) => c) μ
theorem MeasureTheory.locallyIntegrableOn_const {X : Type u_1} {E : Type u_3} [] [] {μ : } {s : Set X} (c : E) :
MeasureTheory.LocallyIntegrableOn (fun (x : X) => c) s μ
theorem MeasureTheory.locallyIntegrable_zero {X : Type u_1} {E : Type u_3} [] [] {μ : } :
MeasureTheory.LocallyIntegrable (fun (x : X) => 0) μ
theorem MeasureTheory.locallyIntegrableOn_zero {X : Type u_1} {E : Type u_3} [] [] {μ : } {s : Set X} :
MeasureTheory.LocallyIntegrableOn (fun (x : X) => 0) s μ
theorem MeasureTheory.LocallyIntegrable.indicator {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } (hf : ) {s : Set X} (hs : ) :
theorem MeasureTheory.locallyIntegrable_map_homeomorph {X : Type u_1} {Y : Type u_2} {E : Type u_3} [] [] [] [] [] [] (e : X ≃ₜ Y) {f : YE} {μ : } :
theorem MeasureTheory.LocallyIntegrable.add {X : Type u_1} {E : Type u_3} [] [] {f : XE} {g : XE} {μ : } (hf : ) (hg : ) :
theorem MeasureTheory.LocallyIntegrable.sub {X : Type u_1} {E : Type u_3} [] [] {f : XE} {g : XE} {μ : } (hf : ) (hg : ) :
theorem MeasureTheory.LocallyIntegrable.neg {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } (hf : ) :
theorem MeasureTheory.LocallyIntegrable.smul {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {𝕜 : Type u_6} [] [] (hf : ) (c : 𝕜) :
theorem MeasureTheory.locallyIntegrable_finset_sum' {X : Type u_1} {E : Type u_3} [] [] {μ : } {ι : Type u_6} (s : ) {f : ιXE} (hf : is, ) :
MeasureTheory.LocallyIntegrable (∑ is, f i) μ
theorem MeasureTheory.locallyIntegrable_finset_sum {X : Type u_1} {E : Type u_3} [] [] {μ : } {ι : Type u_6} (s : ) {f : ιXE} (hf : is, ) :
MeasureTheory.LocallyIntegrable (fun (a : X) => is, f i a) μ
theorem MeasureTheory.LocallyIntegrable.integrable_smul_left_of_hasCompactSupport {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } [] [] (hf : ) {g : X} (hg : ) (h'g : ) :
MeasureTheory.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_3} [] [] {μ : } [] [] {f : X} (hf : ) {g : XE} (hg : ) (h'g : ) :
MeasureTheory.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} {E : Type u_3} [] [] {f : XE} {μ : } :
theorem MeasureTheory.integrable_iff_integrableAtFilter_atBot_atTop {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } [] [] :
theorem MeasureTheory.integrable_iff_integrableAtFilter_atBot {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } [] [] [] :
theorem MeasureTheory.integrable_iff_integrableAtFilter_atTop {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } [] [] [] :
theorem MeasureTheory.integrableOn_Iic_iff_integrableAtFilter_atBot {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {a : X} [] [] :
theorem MeasureTheory.integrableOn_Ici_iff_integrableAtFilter_atTop {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {a : X} [] [] :
theorem MeasureTheory.integrableOn_Iio_iff_integrableAtFilter_atBot_nhdsWithin {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {a : X} [] [] [] [] :
theorem MeasureTheory.integrableOn_Ioi_iff_integrableAtFilter_atTop_nhdsWithin {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {a : X} [] [] [] [] :
theorem Continuous.locallyIntegrable {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } (hf : ) :

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} [] [] {f : XE} {μ : } {K : Set X} (hf : ) (hK : ) :

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} [] [] {f : XE} {μ : } {K : Set X} (hK : ) (h'K : ) (hf : ) :

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_3} [] [] {f : XE} {μ : } {K : Set X} [] (hK : ) (hf : ) :
theorem ContinuousOn.integrableOn_Icc {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {a : X} {b : X} [] [] [] (hf : ContinuousOn f (Set.Icc a b)) :
theorem Continuous.integrableOn_Icc {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {a : X} {b : X} [] [] [] (hf : ) :
theorem Continuous.integrableOn_Ioc {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {a : X} {b : X} [] [] [] (hf : ) :
theorem ContinuousOn.integrableOn_uIcc {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {a : X} {b : X} [] [] [] (hf : ContinuousOn f (Set.uIcc a b)) :
theorem Continuous.integrableOn_uIcc {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {a : X} {b : X} [] [] [] (hf : ) :
theorem Continuous.integrableOn_uIoc {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {a : X} {b : X} [] [] [] (hf : ) :
theorem Continuous.integrable_of_hasCompactSupport {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } (hf : ) (hcf : ) :

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} [] [] {f : XE} {μ : } {s : Set X} [] [] [] (hmono : ) {a : X} {b : X} (ha : IsLeast s a) (hb : ) (hs : μ s ) (h's : ) :
theorem MonotoneOn.integrableOn_isCompact {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {s : Set X} [] [] [] (hs : ) (hmono : ) :
theorem AntitoneOn.integrableOn_of_measure_ne_top {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {s : Set X} [] [] [] (hanti : ) {a : X} {b : X} (ha : IsLeast s a) (hb : ) (hs : μ s ) (h's : ) :
theorem AntioneOn.integrableOn_isCompact {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } {s : Set X} [] [] [] (hs : ) (hanti : ) :
theorem Monotone.locallyIntegrable {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } [] [] [] (hmono : ) :
theorem Antitone.locallyIntegrable {X : Type u_1} {E : Type u_3} [] [] {f : XE} {μ : } [] [] [] (hanti : ) :
theorem MeasureTheory.IntegrableOn.mul_continuousOn_of_subset {X : Type u_1} {R : Type u_5} [] [] {μ : } {A : Set X} {K : Set X} [] {g : XR} {g' : XR} (hg : ) (hg' : ContinuousOn g' K) (hA : ) (hK : ) (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} [] [] {μ : } {K : Set X} [] {g : XR} {g' : XR} [] (hg : ) (hg' : ContinuousOn g' K) (hK : ) :
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} [] [] {μ : } {A : Set X} {K : Set X} [] {g : XR} {g' : XR} (hg : ) (hg' : ) (hK : ) (hA : ) (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} [] [] {μ : } {K : Set X} [] {g : XR} {g' : XR} [] (hg : ) (hg' : ) (hK : ) :
MeasureTheory.IntegrableOn (fun (x : X) => g x * g' x) K μ
theorem MeasureTheory.IntegrableOn.continuousOn_smul {X : Type u_1} {E : Type u_3} [] [] {μ : } {K : Set X} {𝕜 : Type u_6} [] [] [] {g : XE} (hg : ) {f : X𝕜} (hf : ) (hK : ) :
MeasureTheory.IntegrableOn (fun (x : X) => f x g x) K μ
theorem MeasureTheory.IntegrableOn.smul_continuousOn {X : Type u_1} {E : Type u_3} [] [] {μ : } {K : Set X} {𝕜 : Type u_6} [] [] [] {f : X𝕜} (hf : ) {g : XE} (hg : ) (hK : ) :
MeasureTheory.IntegrableOn (fun (x : X) => f x g x) K μ
theorem MeasureTheory.LocallyIntegrableOn.continuousOn_mul {X : Type u_1} {R : Type u_5} [] [] {μ : } [] [] {f : XR} {g : XR} {s : Set X} (hf : ) (hg : ) (hs : ) :
MeasureTheory.LocallyIntegrableOn (fun (x : X) => g x * f x) s μ
theorem MeasureTheory.LocallyIntegrableOn.mul_continuousOn {X : Type u_1} {R : Type u_5} [] [] {μ : } [] [] {f : XR} {g : XR} {s : Set X} (hf : ) (hg : ) (hs : ) :
MeasureTheory.LocallyIntegrableOn (fun (x : X) => f x * g x) s μ
theorem MeasureTheory.LocallyIntegrableOn.continuousOn_smul {X : Type u_1} {E : Type u_3} [] [] {μ : } [] {𝕜 : Type u_6} [] [] {f : XE} {g : X𝕜} {s : Set X} (hs : ) (hf : ) (hg : ) :
MeasureTheory.LocallyIntegrableOn (fun (x : X) => g x f x) s μ
theorem MeasureTheory.LocallyIntegrableOn.smul_continuousOn {X : Type u_1} {E : Type u_3} [] [] {μ : } [] {𝕜 : Type u_6} [] [] {f : X𝕜} {g : XE} {s : Set X} (hs : ) (hf : ) (hg : ) :
MeasureTheory.LocallyIntegrableOn (fun (x : X) => f x g x) s μ