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_eq_norm_neg: If f is locally integrable, ‖f(-x)‖ = ‖f(x)‖, and f =O[atTop] g for some g integrable atTop, then f is integrable.

theorem MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_eq_norm_neg {α : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] {f : α → E} {g : α → F} {μ : Measure α} [TopologicalSpace α] [SecondCountableTopology α] [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [CompactIccSpace α] [Filter.atTop.IsMeasurablyGenerated] [MeasurableNeg α] [μ.IsNegInvariant] (hf : LocallyIntegrable f μ) (hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg) (ho : f =O[Filter.atTop] g) (hg : IntegrableAtFilter g Filter.atTop μ) : 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.