volume_closedBall — Mathlib

English

For E with Haar measure μ, the unit ball measure equals a gamma-integral expression: μ(ball 0 1) = Γ-based constant times ∫ e^{-||x||^p} dμ.

Русский

Мера единичного шара равна гамма-интегралу: μ(ball 0 1) = константа гамма, умноженная на интеграл e^{-||x||^p} dμ.

LaTeX

$$$\mu(\mathrm{ball}\,0\,1) = \mathrm{OfReal}\left( \frac{ \int_E e^{-\|x\|^p} d\mu(x) }{ \Gamma( \mathrm{finrank}(E) / p + 1 ) } \right)$$$

Lean4

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

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