Documentation

Mathlib.MeasureTheory.Integral.Asymptotics

Bounding of integrals by asymptotics #

We establish integrability of f from f = O(g).

Main results #

theorem Asymptotics.IsBigO.integrableAtFilter {α : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] {f : αE} {g : αF} {μ : MeasureTheory.Measure α} {l : Filter α} [l.IsMeasurablyGenerated] (hf : f =O[l] g) (hfm : StronglyMeasurableAtFilter f l μ) (hg : MeasureTheory.IntegrableAtFilter g l μ) :

If f = O[l] g on measurably generated l, f is strongly measurable at l, and g is integrable at l, then f is integrable at l.

theorem Asymptotics.IsBigO.integrable {α : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] {f : αE} {g : αF} {μ : MeasureTheory.Measure α} (hfm : MeasureTheory.AEStronglyMeasurable f μ) (hf : f =O[] g) (hg : MeasureTheory.Integrable g μ) :

Variant of MeasureTheory.Integrable.mono taking f =O[⊤] (g) instead of ‖f(x)‖ ≤ ‖g(x)‖

If f is locally integrable, and f =O[cocompact] g for some g integrable at cocompact, then f is integrable.

theorem MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atBot_atTop {α : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] {f : αE} {g : αF} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [CompactIccSpace α] {g' : αF} [Filter.atBot.IsMeasurablyGenerated] [Filter.atTop.IsMeasurablyGenerated] (hf : MeasureTheory.LocallyIntegrable f μ) (ho : f =O[Filter.atBot] g) (hg : MeasureTheory.IntegrableAtFilter g Filter.atBot μ) (ho' : f =O[Filter.atTop] g') (hg' : MeasureTheory.IntegrableAtFilter g' Filter.atTop μ) :

If f is locally integrable, and f =O[atBot] g, f =O[atTop] g' for some g, g' integrable at atBot and atTop respectively, then f is integrable.

theorem MeasureTheory.LocallyIntegrableOn.integrableOn_of_isBigO_atBot {α : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] {f : αE} {g : αF} {a : α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [CompactIccSpace α] [Filter.atBot.IsMeasurablyGenerated] (hf : MeasureTheory.LocallyIntegrableOn f (Set.Iic a) μ) (ho : f =O[Filter.atBot] g) (hg : MeasureTheory.IntegrableAtFilter g Filter.atBot μ) :

If f is locally integrable on (∞, a], and f =O[atBot] g, for some g integrable at atBot, then f is integrable on (∞, a].

theorem MeasureTheory.LocallyIntegrableOn.integrableOn_of_isBigO_atTop {α : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] {f : αE} {g : αF} {a : α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [CompactIccSpace α] [Filter.atTop.IsMeasurablyGenerated] (hf : MeasureTheory.LocallyIntegrableOn f (Set.Ici a) μ) (ho : f =O[Filter.atTop] g) (hg : MeasureTheory.IntegrableAtFilter g Filter.atTop μ) :

If f is locally integrable on [a, ∞), and f =O[atTop] g, for some g integrable at atTop, then f is integrable on [a, ∞).

theorem MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atBot {α : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] {f : αE} {g : αF} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [CompactIccSpace α] [Filter.atBot.IsMeasurablyGenerated] [OrderTop α] (hf : MeasureTheory.LocallyIntegrable f μ) (ho : f =O[Filter.atBot] g) (hg : MeasureTheory.IntegrableAtFilter g Filter.atBot μ) :

If f is locally integrable, f has a top element, and f =O[atBot] g, for some g integrable at atBot, then f is integrable.

theorem MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop {α : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] {f : αE} {g : αF} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [CompactIccSpace α] [Filter.atTop.IsMeasurablyGenerated] [OrderBot α] (hf : MeasureTheory.LocallyIntegrable f μ) (ho : f =O[Filter.atTop] g) (hg : MeasureTheory.IntegrableAtFilter g Filter.atTop μ) :

If f is locally integrable, f has a bottom element, and f =O[atTop] g, for some g integrable at atTop, then f is integrable.

theorem MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_isNegInvariant {α : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] {f : αE} {g : αF} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [SecondCountableTopology α] [LinearOrderedAddCommGroup α] [CompactIccSpace α] [Filter.atTop.IsMeasurablyGenerated] [MeasurableNeg α] [μ.IsNegInvariant] (hf : MeasureTheory.LocallyIntegrable f μ) (hsymm : norm f =ᵐ[μ] norm f Neg.neg) (ho : f =O[Filter.atTop] g) (hg : MeasureTheory.IntegrableAtFilter g Filter.atTop μ) :

If f is locally integrable, ‖f(-x)‖ = ‖f(x)‖, and f =O[atTop] g, for some g integrable at atTop, then f is integrable.