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} [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 μ) : 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)‖

theorem MeasureTheory.LocallyIntegrable.integrable_of_isBigO_cocompact {α : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] {f : α → E} {g : α → F} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [SecondCountableTopology α] [(Filter.cocompact α).IsMeasurablyGenerated] (hf : MeasureTheory.LocallyIntegrable f μ) (ho : f =O[Filter.cocompact α] g) (hg : MeasureTheory.IntegrableAtFilter g (Filter.cocompact α) μ) : MeasureTheory.Integrable f μ

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 μ) : MeasureTheory.Integrable f μ

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 μ) : MeasureTheory.IntegrableOn f (Set.Iic a) μ

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 μ) : MeasureTheory.IntegrableOn f (Set.Ici a) μ

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 μ) : MeasureTheory.Integrable f μ

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 μ) : MeasureTheory.Integrable f μ

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 μ) : MeasureTheory.Integrable f μ

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