English
Let s be a measurable subset. Then for μ-almost every x, the limit of μ(s ∩ a)/μ(a) as a shrinks to x along a Vitali family equals s.indicator(1,x) (i.e., 1 if x ∈ s and 0 otherwise). This expresses that almost every point of s is a Lebesgue density point of s.
Русский
Пусть s — измеримое множество. Тогда для почти всех x по μ предел μ(s ∩ a)/μ(a) при сжатии a к x вдоль семейства Витали равен индикатору x ∈ s, т.е. 1, если x ∈ s, и 0 иначе. Это выражает, что почти каждая точка множества s является точкой Лебега плотности для s.
LaTeX
$$$\forall x\ \text{μ-a.e. } x,\ Tendsto\bigl(\lambda a.\dfrac{μ(s \cap a)}{μ(a)}\bigr)(v.filterAt x)\bigl(\mathcal{N}(s\text{.indicator}(1,x))\bigr).$$$
Lean4
/-- Given a measurable set `s`, then `μ (s ∩ a) / μ a` converges when `a` shrinks to a typical
point `x` along a Vitali family. 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 {s : Set α} (hs : MeasurableSet s) :
∀ᵐ x ∂μ, Tendsto (fun a => μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 (s.indicator 1 x)) :=
by
haveI : IsLocallyFiniteMeasure (μ.restrict s) := isLocallyFiniteMeasure_of_le restrict_le_self
filter_upwards [ae_tendsto_rnDeriv v (μ.restrict s), rnDeriv_restrict_self μ hs]
intro x hx h'x
simpa only [h'x, restrict_apply' hs, inter_comm] using hx
