Theorems · Theorem · measure theory

MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atBot

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

Defined in

Mathlib.MeasureTheory.Integral.Asymptotics

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupTopologicalSpaceSecondCountableTopologyMeasurableSpaceNormedAddCommGroupLinearOrderCompactIccSpaceFilter.IsMeasurablyGeneratedOrderTop