addHaar_ball — Mathlib

English

Let μ be a Haar measure on a nontrivial finite-dimensional real vector space E. If r ≥ 0, then μ(ball x r) = ENNReal.ofReal(r^finrank E) · μ(ball 0 1).

Русский

Пусть μ — мера Хаара на ненулевом конечномерном вещественном пространстве E. При r ≥ 0 верно: μ(ball x r) = ENNReal.ofReal(r^finrank E) · μ(ball 0 1).

LaTeX

$$$\mu(ball(x, r)) = ENNReal.ofReal\left(r^{\mathrm{finrank}\,\mathbb{R} E}\right) \cdot \mu(ball(0, 1))$$$

Lean4

theorem addHaar_ball [Nontrivial E] (x : E) {r : ℝ} (hr : 0 ≤ r) :
    μ (ball x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 1) := by rw [← addHaar_ball_mul μ x hr, mul_one]

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