English
Let E be a finite-dimensional real inner product space with finrank_R E = 2k+1. Then for all x in E and r in R, the volume of the open ball satisfies vol(ball(x,r)) = |r|^{2k+1} · π^{k} · 2^{k+1} / (2k+1)!!.
Русский
Пусть E — конечномерное вещественное евклидово пространство размерности 2k+1. Тогда для любых x ∈ E и r ∈ R объём шара (окружности) равен vol(ball(x,r)) = |r|^{2k+1} · π^{k} · 2^{k+1} / (2k+1)!!.
LaTeX
$$$$ \operatorname{vol}(\text{ball}(x,r)) = |r|^{2k+1} \cdot \frac{\pi^{k} \cdot 2^{k+1}}{(2k+1)!!}, \quad \text{где } \dim_{\mathbb{R}} E = 2k+1. $$$$
Lean4
theorem volume_ball_of_dim_odd {k : ℕ} (hk : finrank ℝ E = 2 * k + 1) (x : E) (r : ℝ) :
volume (ball x r) = .ofReal r ^ finrank ℝ E * .ofReal (π ^ k * 2 ^ (k + 1) / (finrank ℝ E : ℕ)‼) :=
by
have : Nontrivial E := Module.nontrivial_of_finrank_pos (R := ℝ) (hk ▸ (2 * k).succ_pos)
rw [volume_ball, hk, pow_succ (√π), pow_mul, sq_sqrt pi_nonneg, mul_div_assoc, mul_div_assoc]
congr 3
suffices √π / (↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)) = 2 ^ (k + 1) / ↑(2 * k + 1)‼ by
simpa [add_div, add_right_comm, -one_div, Gamma_nat_add_one_add_half]
field_simp
