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.

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 α} [Filter.IsMeasurablyGenerated l] (hf : f =O[l] g) (hfm : StronglyMeasurableAtFilter f l μ) (hg : MeasureTheory.IntegrableAtFilter g l μ) : MeasureTheory.IntegrableAtFilter f 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 μ) : MeasureTheory.Integrable f μ

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