# Bounding of integrals by asymptotics #

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

## Main results #

• Asymptotics.IsBigO.integrableAtFilter: 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.
• MeasureTheory.LocallyIntegrable.integrable_of_isBigO_cocompact: If f is locally integrable, and f =O[cocompact] g for some g integrable at cocompact, then f is integrable.
• MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atBot_atTop: If f is locally integrable, and f =O[atBot] g, f =O[atTop] g' for some g, g' integrable atBot and atTop respectively, then f is integrable.
• MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_isNegInvariant: If f is locally integrable, ‖f(-x)‖ = ‖f(x)‖, and f =O[atTop] g for some g integrable atTop, then f is integrable.
theorem Asymptotics.IsBigO.integrableAtFilter {α : Type u_1} {E : Type u_2} {F : Type u_3} [] {f : αE} {g : αF} {μ : } {l : } [l.IsMeasurablyGenerated] (hf : f =O[l] g) (hfm : ) (hg : ) :

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} [] {f : αE} {g : αF} {μ : } (hfm : ) (hf : f =O[] g) (hg : ) :

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

theorem MeasureTheory.LocallyIntegrable.integrable_of_isBigO_cocompact {α : Type u_1} {E : Type u_2} {F : Type u_3} [] {f : αE} {g : αF} {μ : } [] [().IsMeasurablyGenerated] (hf : ) (ho : ) (hg : ) :

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} [] {f : αE} {g : αF} {μ : } [] [] [] {g' : αF} [Filter.atBot.IsMeasurablyGenerated] [Filter.atTop.IsMeasurablyGenerated] (hf : ) (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} [] {f : αE} {g : αF} {a : α} {μ : } [] [] [] [Filter.atBot.IsMeasurablyGenerated] (hf : ) (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} [] {f : αE} {g : αF} {a : α} {μ : } [] [] [] [Filter.atTop.IsMeasurablyGenerated] (hf : ) (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} [] {f : αE} {g : αF} {μ : } [] [] [] [Filter.atBot.IsMeasurablyGenerated] [] (hf : ) (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} [] {f : αE} {g : αF} {μ : } [] [] [] [Filter.atTop.IsMeasurablyGenerated] [] (hf : ) (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} [] {f : αE} {g : αF} {μ : } [] [] [Filter.atTop.IsMeasurablyGenerated] [] [μ.IsNegInvariant] (hf : ) (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.