English
Let μ be a Haar measure on a finite-dimensional real vector space E. For hr ≥ 0 and hs ≥ 0, we have μ(closedBall x (hr·hs)) = ENNReal.ofReal((hr)^finrank E) · μ(closedBall 0 hs).
Русский
Пусть μ — мера Хаара на конечномерном пространстве E. При hr ≥ 0 и hs ≥ 0 выполняется: μ(closedBall x (hr·hs)) = ENNReal.ofReal((hr)^finrank E) · μ(closedBall 0 hs).
LaTeX
$$$\mu(closedBall(x, r \cdot s)) = ENNReal.ofReal\left(r^{\mathrm{finrank}\,\mathbb{R} E}\right) \cdot \mu(closedBall(0, s))$$$
Lean4
theorem addHaar_closedBall_mul (x : E) {r : ℝ} (hr : 0 ≤ r) {s : ℝ} (hs : 0 ≤ s) :
μ (closedBall x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 s) :=
by
have : closedBall (0 : E) (r * s) = r • closedBall (0 : E) s := by
simp [smul_closedBall r (0 : E) hs, abs_of_nonneg hr]
simp only [this, addHaar_smul, abs_of_nonneg hr, addHaar_closedBall_center, abs_pow]
