English
Let μ be a Haar measure on a finite-dimensional real vector space E. For any x ∈ E and r ≥ 0 and s ∈ ℝ, the closed- ball scaling holds: μ(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 [Nontrivial E] (x : E) {r : ℝ} (hr : 0 ≤ r) (s : ℝ) :
μ (ball x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 s) :=
by
rcases hr.eq_or_lt with (rfl | h)
· simp only [zero_pow (finrank_pos (R := ℝ) (M := E)).ne', measure_empty, zero_mul, ENNReal.ofReal_zero, ball_zero]
· exact addHaar_ball_mul_of_pos μ x h s
