Theorems · Theorem · measure theory

MeasureTheory.integrableOn_ball_of_norm_le_rpow

∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] [inst_5 : NormedAddCommGroup F] {μ : MeasureTheory.Measure E}
  [μ.IsAddHaarMeasure],
  1 ≤ Module.finrank ℝ E →
    ∀ {f : E → F} {C α r : ℝ},
      α < ↑(Module.finrank ℝ E) →
        (∀ᵐ (x : E) ∂μ.restrict (Metric.ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)) →
          MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.IntegrableOn f (Metric.ball 0 r) μ

Defined in

Mathlib.Analysis.SpecialFunctions.Pow.Integral

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalMeasurableSpaceBorelSpaceNormedAddCommGroupMeasureTheory.Measure.IsAddHaarMeasure