English
The Vitali family is a systematic way to select shrinking sets around each point, satisfying doubling-type covering constraints.
Русский
Семейство Витали задаёт способ выбора сужающихся окрестностей точки при соблюдении ограничений на покрытие.
LaTeX
$$$\text{VitaliFamily } μ\, :=\; \text{a structure with setsAt, filterAt, etc.}$$$
Lean4
/-- *Lebesgue differentiation theorem*: for almost every point `x`, the
average of `f` on `a` tends to `f x` as `a` shrinks to `x` along a Vitali family. -/
theorem ae_tendsto_average [NormedSpace ℝ E] [CompleteSpace E] {f : α → E} (hf : LocallyIntegrable f μ) :
∀ᵐ x ∂μ, Tendsto (fun a => ⨍ y in a, f y ∂μ) (v.filterAt x) (𝓝 (f x)) :=
by
filter_upwards [v.ae_tendsto_average_norm_sub hf, v.ae_eventually_measure_pos] with x hx h'x
rw [tendsto_iff_norm_sub_tendsto_zero]
refine squeeze_zero' (Eventually.of_forall fun a => norm_nonneg _) ?_ hx
filter_upwards [h'x, v.eventually_measure_lt_top x, v.eventually_filterAt_integrableOn x hf] with a ha h'a h''a
nth_rw 1 [← setAverage_const ha.ne' h'a.ne (f x)]
simp_rw [setAverage_eq']
rw [← integral_sub]
· exact norm_integral_le_integral_norm _
· exact (integrable_inv_smul_measure ha.ne' h'a.ne).2 h''a
· exact (integrable_inv_smul_measure ha.ne' h'a.ne).2 (integrableOn_const h'a.ne)
