volume_pi_ball — Mathlib

English

Let ι be finite and a : ι → ℝ. For any r > 0, the Lebesgue volume of the product ball equals ENNReal.ofReal ((2 · r)^{|ι|}).

Русский

Пусть ι конечен и a : ι → ℝ. Для любого r > 0 объём произведения шаров равен ENNReal.ofReal ((2·r)^{|ι|}).

LaTeX

$$$$ \\mathrm{volume}(\\mathrm{Metric.ball}\\ a\\ r) = \\mathrm{ENNReal.ofReal}((2 \\cdot r)^{|\\iota|}). $$$$

Lean4

@[simp]
nonrec theorem volume_pi_ball (a : ι → ℝ) {r : ℝ} (hr : 0 < r) :
    volume (Metric.ball a r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι) :=
  by
  simp only [MeasureTheory.volume_pi_ball a hr, volume_ball, Finset.prod_const]
  exact (ENNReal.ofReal_pow (mul_nonneg zero_le_two hr.le) _).symm

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