English
In AddCircle with volume, closed and open balls around a point are equal almost everywhere.
Русский
В AddCircle с объёмом замкнутые и открытые сферы вокруг точки равны почти всюду по мере.
LaTeX
$$$\\text{closedBall } x \\varepsilon =_{\\ae,\\text{volume}} \\text{ball } x \\varepsilon$$$
Lean4
theorem closedBall_ae_eq_ball {x : AddCircle T} {ε : ℝ} : closedBall x ε =ᵐ[volume] ball x ε :=
by
rcases le_or_gt ε 0 with hε | hε
· rw [ball_eq_empty.mpr hε, ae_eq_empty, volume_closedBall, min_eq_right (by linarith [hT.out] : 2 * ε ≤ T),
ENNReal.ofReal_eq_zero]
exact mul_nonpos_of_nonneg_of_nonpos zero_le_two hε
· suffices volume (closedBall x ε) ≤ volume (ball x ε) from
(ae_eq_of_subset_of_measure_ge ball_subset_closedBall this measurableSet_ball.nullMeasurableSet
(measure_ne_top _ _)).symm
have : Tendsto (fun δ => volume (closedBall x δ)) (𝓝[<] ε) (𝓝 <| volume (closedBall x ε)) :=
by
simp_rw [volume_closedBall]
refine ENNReal.tendsto_ofReal (Tendsto.min tendsto_const_nhds <| Tendsto.const_mul _ ?_)
exact nhdsWithin_le_nhds
refine le_of_tendsto this <| mem_of_superset (Ioo_mem_nhdsLT hε) fun r hr ↦ ?_
exact measure_mono (closedBall_subset_ball hr.2)
