English
For an arbitrary set s, the same Vitali-type concentration holds in the sense that μ.restrict s-almost every x has μ(a ∩ s)/μ(a) tend to 1 as a shrinks to x along a Vitali family.
Русский
Для произвольного множества s справедлив аналогичный предел для μ.restrict s: почти для μ-похожих точек x доля μ(a ∩ s)/μ(a) стремится к 1, когда a уменьшается к x вдоль Family Vitali.
LaTeX
$$$\forall^{\mu.restrict s}\ x,\ Tendsto(\lambda a.\dfrac{μ(s ∩ a)}{μ a})(v.filterAt x)(𝓝 1).$$$
Lean4
/-- Given an arbitrary set `s`, then `μ (s ∩ a) / μ a` converges to `1` when `a` shrinks to a
typical point of `s` along a Vitali family. This shows that almost every point of `s` is a
Lebesgue density point for `s`. A stronger version for measurable sets is given
in `ae_tendsto_measure_inter_div_of_measurableSet`. -/
theorem ae_tendsto_measure_inter_div (s : Set α) :
∀ᵐ x ∂μ.restrict s, Tendsto (fun a => μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 1) :=
by
let t := toMeasurable μ s
have A : ∀ᵐ x ∂μ.restrict s, Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x)) :=
by
apply ae_mono restrict_le_self
apply ae_tendsto_measure_inter_div_of_measurableSet
exact measurableSet_toMeasurable _ _
have B : ∀ᵐ x ∂μ.restrict s, t.indicator 1 x = (1 : ℝ≥0∞) :=
by
refine ae_restrict_of_ae_restrict_of_subset (subset_toMeasurable μ s) ?_
filter_upwards [ae_restrict_mem (measurableSet_toMeasurable μ s)] with _ hx
simp only [t, hx, Pi.one_apply, indicator_of_mem]
filter_upwards [A, B] with x hx h'x
rw [h'x] at hx
apply hx.congr' _
filter_upwards [v.eventually_filterAt_measurableSet x] with _ ha
congr 1
exact measure_toMeasurable_inter_of_sFinite ha _
