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} [NormedAddCommGroup E] {f : α → E} {g : α → F} {l : Filter α} [MeasurableSpace α] [NormedAddCommGroup F] {μ : MeasureTheory.Measure α} [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} [NormedAddCommGroup E] {f : α → E} {g : α → F} [MeasurableSpace α] [NormedAddCommGroup 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 Asymptotics.IsBigO.eventually_integrableOn {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] {g : α → F} {l : Filter α} {ι : Type u_4} [MeasurableSpace ι] {f : ι × α → E} {s : Set ι} {μ : MeasureTheory.Measure ι} [Norm F] (hf : f =O[Filter.principal s ×ˢ l] (g ∘ Prod.snd)) (hfm : ∀ᶠ (x : α) in l, MeasureTheory.AEStronglyMeasurable (fun (i : ι) => f (i, x)) (μ.restrict s)) (hs : MeasurableSet s) (hμ : μ s < ⊤) : ∀ᶠ (x : α) in l, MeasureTheory.IntegrableOn (fun (i : ι) => f (i, x)) s μ

Let f : X x Y → Z. If as y tends to l, f(x, y) = O(g(y)) uniformly on s : Set X of finite measure, then f is eventually (as y tends to l) integrable along s.

theorem Asymptotics.IsBigO.set_integral_isBigO {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] {g : α → F} {l : Filter α} {ι : Type u_4} [MeasurableSpace ι] {f : ι × α → E} {s : Set ι} {μ : MeasureTheory.Measure ι} [NormedSpace ℝ E] [NormedAddCommGroup F] (hf : f =O[Filter.principal s ×ˢ l] (g ∘ Prod.snd)) (hs : MeasurableSet s) (hμ : μ s < ⊤) : (fun (x : α) => ∫ (i : ι) in s, f (i, x) ∂μ) =O[l] g

Let f : X x Y → Z. If as y tends to l, f(x, y) = O(g(y)) uniformly on s : Set X of finite measure, then the integral of f along s is O(g(y)).

theorem MeasureTheory.LocallyIntegrable.integrable_of_isBigO_cocompact {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] {f : α → E} {g : α → F} [TopologicalSpace α] [SecondCountableTopology α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [(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} [NormedAddCommGroup E] {f : α → E} {g : α → F} [TopologicalSpace α] [SecondCountableTopology α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [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} [NormedAddCommGroup E] {f : α → E} {g : α → F} {a : α} [TopologicalSpace α] [SecondCountableTopology α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [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} [NormedAddCommGroup E] {f : α → E} {g : α → F} {a : α} [TopologicalSpace α] [SecondCountableTopology α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [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} [NormedAddCommGroup E] {f : α → E} {g : α → F} [TopologicalSpace α] [SecondCountableTopology α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [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} [NormedAddCommGroup E] {f : α → E} {g : α → F} [TopologicalSpace α] [SecondCountableTopology α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [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} [NormedAddCommGroup E] {f : α → E} {g : α → F} [TopologicalSpace α] [SecondCountableTopology α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [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.