Theorems · Theorem · measure theory

MeasureTheory.measure_unitBall_eq_integral_div_gamma

∀ {E : Type u_1} {p : ℝ} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure],
  0 < p →
    μ (Metric.ball 0 1) =
      ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma (↑(Module.finrank ℝ E) / p + 1))

Defined in

Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsAddHaarMeasure