English
In AddCircle T, the Haar measure of a closed ball of radius ε around any point x equals ENNReal.ofReal(min(T, 2ε)).
Русский
В AddCircle(T) мера Хаара шарa радиуса ε вокруг точки x равна ENNReal.ofReal(min(T, 2ε)).
LaTeX
$$$\\mathrm{vol}(\\mathrm{Metric.closedBall}(x,\\varepsilon))=\\mathrm{ENNReal}.\\mathrm{ofReal}(\\min\\{T,2\\varepsilon\\})$$$
Lean4
theorem volume_closedBall {x : AddCircle T} (ε : ℝ) : volume (Metric.closedBall x ε) = ENNReal.ofReal (min T (2 * ε)) :=
by
have hT' : |T| = T := abs_eq_self.mpr hT.out.le
let I := Ioc (-(T / 2)) (T / 2)
have h₁ : ε < T / 2 → Metric.closedBall (0 : ℝ) ε ∩ I = Metric.closedBall (0 : ℝ) ε :=
by
intro hε
rw [inter_eq_left, Real.closedBall_eq_Icc, zero_sub, zero_add]
rintro y ⟨hy₁, hy₂⟩; constructor <;> linarith
have h₂ : (↑) ⁻¹' Metric.closedBall (0 : AddCircle T) ε ∩ I = if ε < T / 2 then Metric.closedBall (0 : ℝ) ε else I :=
by
conv_rhs => rw [← if_ctx_congr (Iff.rfl : ε < T / 2 ↔ ε < T / 2) h₁ fun _ => rfl, ← hT']
apply coe_real_preimage_closedBall_inter_eq
simpa only [hT', Real.closedBall_eq_Icc, zero_add, zero_sub] using Ioc_subset_Icc_self
rw [addHaar_closedBall_center, add_projection_respects_measure T (-(T / 2)) measurableSet_closedBall,
(by linarith : -(T / 2) + T = T / 2), h₂]
by_cases hε : ε < T / 2
· simp [hε, min_eq_right (by linarith : 2 * ε ≤ T)]
· simp [I, hε, min_eq_left (by linarith : T ≤ 2 * ε)]
