volume_closedBall_of_dim_even — Mathlib

English

Let E be a finite-dimensional real inner product space. If finrank_R E = 2k, then for every x in E and r in R, the volume of the closed ball centered at x with radius r is vol(closedBall(x,r)) = |r|^{2k} · π^{k} / k!.

Русский

Пусть E — конечномерное вещественное евклидово пространство. Пусть dim_R E = 2k. Тогда для любых x ∈ E и r ∈ R объём замкнутого шара centered at x с радиусом r равен vol(closedBall(x,r)) = |r|^{2k} · π^{k} / k!.

LaTeX

$$$$ \operatorname{vol}(\overline{B}(x,r)) = |r|^{2k} \cdot \frac{\pi^{k}}{k!}, \quad \text{где } \dim_{\mathbb{R}} E = 2k. $$$$

Lean4

theorem volume_closedBall_of_dim_even {k : ℕ} (hk : finrank ℝ E = 2 * k) (x : E) (r : ℝ) :
    volume (closedBall x r) = .ofReal r ^ finrank ℝ E * .ofReal (π ^ k / (k : ℕ)!) := by
  rw [addHaar_closedBall_eq_addHaar_ball, volume_ball_of_dim_even hk x]

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