English
Let μ be a Haar measure on a finite-dimensional real vector space E. Then for every x in E and every radius r in R, the real-valued measure μ_real of the closed ball centered at x with radius r equals the real-valued measure of the closed ball centered at 0 with the same radius, i.e. μ.real(closedBall(x, r)) = μ.real(closedBall(0, r)).
Русский
Пусть μ — мера Хаара на конечномерном вещественном векторном пространстве E. Тогда для любого x ∈ E и любого радиуса r ∈ ℝ выполнено: μ.real(closedBall(x, r)) = μ.real(closedBall(0, r)).
LaTeX
$$$\mu_{\mathbb{R}}(\overline{B}(x,r)) = \mu_{\mathbb{R}}(\overline{B}(0,r))$$$
Lean4
theorem addHaar_real_closedBall_center {E : Type*} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E]
(μ : Measure E) [IsAddHaarMeasure μ] (x : E) (r : ℝ) : μ.real (closedBall x r) = μ.real (closedBall (0 : E) r) := by
simp [measureReal_def, addHaar_closedBall_center]
