volume_closedBall — Mathlib

English

In an inner product space E, the volume of the Euclidean ball B(x,r) equals r^{dim E} times a gamma-based constant depending on dim E.

Русский

В пространстве с скалярным произведением измеримый объем шара B(x,r) пропорционален r^{dim E} с гамма-константой зависимой от размерности.

LaTeX

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

Lean4

theorem volume_closedBall (x : E) (r : ℝ) :
    volume (Metric.closedBall x r) =
      (.ofReal r) ^ finrank ℝ E * .ofReal (√π ^ finrank ℝ E / Gamma (finrank ℝ E / 2 + 1)) :=
  by rw [addHaar_closedBall_eq_addHaar_ball, InnerProductSpace.volume_ball _]

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