Theorems · Theorem · measure theory

InnerProductSpace.volume_ball_of_dim_odd

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {k : ℕ},
  Module.finrank ℝ E = 2 * k + 1 →
    ∀ (x : E) (r : ℝ),
      MeasureTheory.volume (Metric.ball x r) =
        ENNReal.ofReal r ^ Module.finrank ℝ E *
          ENNReal.ofReal (Real.pi ^ k * 2 ^ (k + 1) / ↑(Module.finrank ℝ E).doubleFactorial)

Defined in

Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceFiniteDimensionalMeasurableSpaceBorelSpace