Theorems · Theorem · measure theory

MeasureTheory.LocallyIntegrableOn.integrableOn_of_isBigO_atTop

∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] {f : α → E} {g : α → F} {a : α}
  [inst_1 : TopologicalSpace α] [SecondCountableTopology α] [inst_3 : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_4 : NormedAddCommGroup F] [inst_5 : LinearOrder α] [CompactIccSpace α] [Filter.atTop.IsMeasurablyGenerated],
  MeasureTheory.LocallyIntegrableOn f (Set.Ici a) μ →
    f =O[Filter.atTop] g →
      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, ∞).

Defined in

Mathlib.MeasureTheory.Integral.Asymptotics

Cited by

4 results in Mathlib

Foundations

Depth 214 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupTopologicalSpaceSecondCountableTopologyMeasurableSpaceNormedAddCommGroupLinearOrderCompactIccSpaceFilter.IsMeasurablyGenerated