English
For Nontrivial E and any x and r ≥ 0, the real-valued measure μ.real of the closed ball satisfies μ.real(closedBall x r) = r^finrank E · μ.real(closedBall 0 1).
Русский
Для ненулевого пространства E и любых x и r ≥ 0 верно: μ.real(closedBall x r) = r^finrank E · μ.real(closedBall(0,1)).
LaTeX
$$$\mu_{\mathbb{R}}(\overline{B}(x, r)) = r^{\mathrm{finrank}\,\mathbb{R} E} \cdot \mu_{\mathbb{R}}(\overline{B}(0, 1))$$$
Lean4
/-- The measure of a closed ball can be expressed in terms of the measure of the closed unit ball.
Use instead `addHaar_closedBall`, which uses the measure of the open unit ball as a standard
form. -/
theorem addHaar_closedBall' (x : E) {r : ℝ} (hr : 0 ≤ r) :
μ (closedBall x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 1) := by
rw [← addHaar_closedBall_mul μ x hr zero_le_one, mul_one]
