addHaar_ball_of_pos — Mathlib

English

Let μ be a Haar measure on a finite-dimensional real vector space E. If r > 0, then the ball of radius r around x has measure μ(ball x r) = ENNReal.ofReal(r^finrank) · μ(ball 0 1).

Русский

Пусть μ — мера Хаара на конечномерном пространстве E. При r > 0 выполнено: μ(ball(x, r)) = ENNReal.ofReal(r^finrank) · μ(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_of_pos (x : E) {r : ℝ} (hr : 0 < r) :
    μ (ball x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 1) := by rw [← addHaar_ball_mul_of_pos μ x hr, mul_one]

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