English
On the real line with volume measure, for any x<y, the interval [x,y] belongs to the Vitali sets-at-x determined by the Vitali family built from volume.
Русский
На вещественной линии с мерой объема для любого x<y промежуток [x,y] принадлежит множеству Vitali, связанного с x.
LaTeX
$$$Icc\,x\,y \in (vitaliFamily(volume) 1).setsAt\ x.$$$
Lean4
/-- *Lebesgue differentiation theorem*: for almost every point `x`, the
average of `‖f y - f x‖` on `a` tends to `0` as `a` shrinks to `x` along a Vitali family. -/
theorem ae_tendsto_average_norm_sub {f : α → E} (hf : LocallyIntegrable f μ) :
∀ᵐ x ∂μ, Tendsto (fun a => ⨍ y in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0) :=
by
filter_upwards [v.ae_tendsto_lintegral_enorm_sub_div hf] with x hx
have := (ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp hx
simp only [ENNReal.toReal_zero] at this
apply Tendsto.congr' _ this
filter_upwards [v.eventually_measure_lt_top x, v.eventually_filterAt_integrableOn x hf] with a h'a h''a
simp only [Function.comp_apply, ENNReal.toReal_div, setAverage_eq, div_eq_inv_mul]
have A : IntegrableOn (fun y => (‖f y - f x‖₊ : ℝ)) a μ :=
by
simp_rw [coe_nnnorm]
exact (h''a.sub (integrableOn_const h'a.ne)).norm
dsimp [enorm]
rw [lintegral_coe_eq_integral _ A, ENNReal.toReal_ofReal (by positivity)]
simp only [coe_nnnorm, measureReal_def]
