English
For Haar measure μ on a finite-dimensional real vector space E, μ(closedBall 0 1) = μ(ball 0 1).
Русский
Для меры Хаара μ на конечномерном пространстве E имеет место равенство μ(closedBall 0 1) = μ(ball 0 1).
LaTeX
$$$\mu(closedBall(0,1)) = \mu(ball(0,1))$$$
Lean4
theorem addHaar_unitClosedBall_eq_addHaar_unitBall : μ (closedBall (0 : E) 1) = μ (ball 0 1) :=
by
apply le_antisymm _ (measure_mono ball_subset_closedBall)
have A :
Tendsto (fun r : ℝ => ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall (0 : E) 1)) (𝓝[<] 1)
(𝓝 (ENNReal.ofReal ((1 : ℝ) ^ finrank ℝ E) * μ (closedBall (0 : E) 1))) :=
by
refine ENNReal.Tendsto.mul ?_ (by simp) tendsto_const_nhds (by simp)
exact ENNReal.tendsto_ofReal ((tendsto_id'.2 nhdsWithin_le_nhds).pow _)
simp only [one_pow, one_mul, ENNReal.ofReal_one] at A
refine le_of_tendsto A ?_
filter_upwards [Ioo_mem_nhdsLT zero_lt_one] with r hr
rw [← addHaar_closedBall' μ (0 : E) hr.1.le]
exact measure_mono (closedBall_subset_ball hr.2)
