volume_ball_of_dim_even — Mathlib

English

In an inner product space E, the volume of the closed ball is the same as that of the open ball up to a gamma-constant, i.e., volume of closedBall equals same r^d multiple as open ball.

Русский

В векторном пространстве с скалярным произведением мера закрытого шара совпадает по модулю (лот) с открытым шаром: объем закрытого шара пропорционален r^d как и объем открытого шара.

LaTeX

$$$\mathrm{volume}(\mathrm{closedBall}\,x\,r) = (\!\,r)^{\mathrm{finrank}\, E} \, \mathrm{ofReal}\left( \frac{\sqrt{\pi}^{\mathrm{finrank}\, E}}{\Gamma(\mathrm{finrank}\, E / 2 + 1)} \right)$$$

Lean4

theorem volume_ball_of_dim_even {k : ℕ} (hk : finrank ℝ E = 2 * k) (x : E) (r : ℝ) :
    volume (ball x r) = .ofReal r ^ finrank ℝ E * .ofReal (π ^ k / (k : ℕ)!) :=
  by
  rw [volume_ball, hk, pow_mul, pow_mul, sq_sqrt pi_nonneg]
  congr
  simp [Gamma_nat_eq_factorial]

Похожие утверждения