English
Let μ be a locally finite measure on β and s a measurable subset. Then for μ-almost every x, the ratio μ(s ∩ closedBall x r) / μ(closedBall x r) tends to s.indicator 1 x as r ↓ 0.
Русский
Пусть μ — локально конечная мера на β и s измеримо. Тогда для почти всех x по μ предел при r→0+ от отношения μ(s ∩ закрытаяшара(x,r)) к μ(закрытаяшара(x,r)) равен индикатору s в x, то есть 1 если x ∈ s, 0 иначе.
LaTeX
$$$$\\forall^{\\ae} x\\; ∂μ,\\; \\ 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}(s.indicator 1\; x)\\right).$$$$
Lean4
/-- Given a measurable set `s`, then `μ (s ∩ closedBall x r) / μ (closedBall x r)` converges when
`r` tends to `0`, for almost every `x`. The limit is `1` for `x ∈ s` and `0` for `x ∉ s`.
This shows that almost every point of `s` is a Lebesgue density point for `s`.
A version for non-measurable sets holds, but it only gives the first conclusion,
see `ae_tendsto_measure_inter_div`. -/
theorem ae_tendsto_measure_inter_div_of_measurableSet (μ : Measure β) [IsLocallyFiniteMeasure μ] {s : Set β}
(hs : MeasurableSet s) :
∀ᵐ x ∂μ, Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 (s.indicator 1 x)) :=
by
filter_upwards [VitaliFamily.ae_tendsto_measure_inter_div_of_measurableSet (Besicovitch.vitaliFamily μ) hs]
intro x hx
exact hx.comp (tendsto_filterAt μ x)
