Theorems · Theorem · measure theory

MeasureTheory.Measure.toSphereBallBound_mul_measureReal_unitBall_le_toSphere_ball

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  (μ : MeasureTheory.Measure E) [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {ε : ℝ},
  0 < ε →
    ∀ (x : ↑(Metric.sphere 0 1)),
      ↑(MeasureTheory.Measure.toSphereBallBound (Module.finrank ℝ E) ε) * μ.real (Metric.ball 0 1) ≤
        μ.toSphere.real (Metric.ball x ε)

A ball of radius ε on the unit sphere in a real normed space has measure at least toSphereBallBound n ε * μ (ball 0 1), where n is the dimension of the space, toSphereBallBound n ε is a lower estimate that depends only on the dimension and ε, which is positive for positive n and ε. This is a version stated in terms MeasureTheory.Measure.real.

Defined in

Mathlib.MeasureTheory.Constructions.HaarToSphere

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceMeasurableSpaceBorelSpaceFiniteDimensionalMeasureTheory.Measure.IsAddHaarMeasure