Theorems · Theorem · measure theory

MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_isNegInvariant

∀ {α : 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 : AddCommGroup α] [inst_6 : LinearOrder α] [IsOrderedAddMonoid α]
  [CompactIccSpace α] [Filter.atTop.IsMeasurablyGenerated] [MeasurableNeg α] [μ.IsNegInvariant],
  MeasureTheory.LocallyIntegrable f μ →
    norm ∘ f =ᵐ[μ] norm ∘ f ∘ Neg.neg →
      f =O[Filter.atTop] g → 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.

Defined in

Mathlib.MeasureTheory.Integral.Asymptotics

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupTopologicalSpaceSecondCountableTopologyMeasurableSpaceNormedAddCommGroupAddCommGroupLinearOrderIsOrderedAddMonoidCompactIccSpaceFilter.IsMeasurablyGeneratedMeasurableNegMeasureTheory.Measure.IsNegInvariant