Theorems · Theorem · measure theory

MeasureTheory.LocallyIntegrableOn.integrableOn_of_isBigO_atBot

∀ {α : 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.atBot.IsMeasurablyGenerated],
  MeasureTheory.LocallyIntegrableOn f (Set.Iic a) μ →
    f =O[Filter.atBot] g →
      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].

Defined in

Mathlib.MeasureTheory.Integral.Asymptotics

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupTopologicalSpaceSecondCountableTopologyMeasurableSpaceNormedAddCommGroupLinearOrderCompactIccSpaceFilter.IsMeasurablyGenerated