English
For a finite index set ι, the measured volume identity holds for the π-volume in terms of an ENNReal expression with Gamma functions, mirroring the even- or odd-dimension constants.
Русский
Для конечного множества индексов ι равенство объема выражено через π-объем и гамму-функции, зеркалирующее размерности пространства.
LaTeX
$$$\text{volume}_{\pi}(\mathbb{R}^ι) = \mathrm{ENNReal.ofReal}\left( \cdot \Gamma(\cdot) \right)$$$
Lean4
theorem volume_ball (x : EuclideanSpace ℝ ι) (r : ℝ) :
volume (Metric.ball x r) = (.ofReal r) ^ card ι * .ofReal (√π ^ card ι / Gamma (card ι / 2 + 1)) :=
by
obtain hr | hr := le_total r 0
· rw [Metric.ball_eq_empty.mpr hr, measure_empty, ← zero_eq_ofReal.mpr hr, zero_pow card_ne_zero, zero_mul]
· suffices volume (Metric.ball (0 : EuclideanSpace ℝ ι) 1) = .ofReal (√π ^ card ι / Gamma (card ι / 2 + 1)) by
rw [Measure.addHaar_ball _ _ hr, this, ofReal_pow hr, finrank_euclideanSpace]
rw [← ((volume_preserving_measurableEquiv _).symm).measure_preimage measurableSet_ball.nullMeasurableSet]
simp only [Set.preimage, ball_zero_eq _ zero_le_one, one_pow, Set.mem_setOf_eq]
convert volume_sum_rpow_lt_one ι one_le_two using 4
· simp [sq_abs, EuclideanSpace.measurableEquiv]
· rw [Gamma_add_one (by simp), Gamma_one_half_eq, ← mul_assoc, mul_div_cancel₀ _ two_ne_zero, one_mul]
