English
Let μ be a Haar measure on a finite-dimensional real vector space E. For any x ∈ E and any r > 0 and s ∈ ℝ, the measure of the ball centered at x with radius r·s scales as ENNReal.ofReal(r^finrank E) times the measure of the ball of radius s centered at 0: μ(ball x (r·s)) = ENNReal.ofReal(r^finrank E) · μ(ball 0 s).
Русский
Пусть μ — мера Хаара на конечномерном вещественном пространстве E. Для любого x ∈ E и любых r > 0, s ∈ ℝ выполняется: μ(ball(x, r·s)) = ENNReal.ofReal(r^finrank E) · μ(ball(0, s)).
LaTeX
$$$\mu(ball(x, r \cdot s)) = ENNReal.ofReal\left(r^{\mathrm{finrank}\,\mathbb{R} E}\right) \cdot \mu(ball(0, s))$$$
Lean4
theorem addHaar_ball_mul_of_pos (x : E) {r : ℝ} (hr : 0 < r) (s : ℝ) :
μ (ball x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 s) :=
by
have : ball (0 : E) (r * s) = r • ball (0 : E) s := by
simp only [_root_.smul_ball hr.ne' (0 : E) s, Real.norm_eq_abs, abs_of_nonneg hr.le, smul_zero]
simp only [this, addHaar_smul, abs_of_nonneg hr.le, addHaar_ball_center, abs_pow]
