English
For any set s (not necessarily measurable), almost every x in μ.restrict s is a Lebesgue density point, i.e., μ(s ∩ closedBall x r)/μ(closedBall x r) → 1 as r ↓ 0.
Русский
Для произвольного множества s (не обязательно измеримого) почти каждая точка x по μ внутри s является точкой плотности Лебега, т.е. отношение μ(s ∩ закрытая_шара(x,r)) к μ(закрытая_шара(x,r)) стремится к 1 при r→0.
LaTeX
$$$$\\forall^{\\ae} x \\partial(μ.restrict s),\\; \\ Tendsto\\left(\\lambda r,\\frac{μ(s \\cap \\overline{B}(x,r))}{μ(\\overline{B}(x,r))}\\right)\\left(\\mathcal{N}_{[>0]}(0)\\right)\\left(\\mathcal{N}(1)\\right).$$$$
Lean4
/-- Given an arbitrary set `s`, then `μ (s ∩ closedBall x r) / μ (closedBall x r)` converges
to `1` when `r` tends to `0`, for almost every `x` in `s`.
This shows that almost every point of `s` is a Lebesgue density point for `s`.
A stronger version holds for measurable sets, see `ae_tendsto_measure_inter_div_of_measurableSet`.
See also `IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div`. -/
theorem ae_tendsto_measure_inter_div (μ : Measure β) [IsLocallyFiniteMeasure μ] (s : Set β) :
∀ᵐ x ∂μ.restrict s, Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1) := by
filter_upwards [VitaliFamily.ae_tendsto_measure_inter_div (Besicovitch.vitaliFamily μ) s] with x hx using
hx.comp (tendsto_filterAt μ x)
