English
Let f be AEMeasurable with respect to μ and not essentially infinite integral; Then the same Vitali-type convergence holds for f.
Русский
Пусть f является AEMeasurable по μ с конечным интегралом; тогда сужение интегралов по мере Витали даёт такое же сходство.
LaTeX
$$$\forall f:\alpha\to\mathbb{R}_{\ge 0},\ \text{AEMeasurable } f\,μ\ Rightarrow\ \forall^{\mu}\ x,\ Tendsto(\lambda a.\int_{y∈a} f(y) dμ / μ(a))(v.filterAt x)\mathcal{N}(f(x)).$$$
Lean4
theorem ae_tendsto_lintegral_div {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) (h'f : (∫⁻ y, f y ∂μ) ≠ ∞) :
∀ᵐ x ∂μ, Tendsto (fun a => (∫⁻ y in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (f x)) :=
by
have A : (∫⁻ y, hf.mk f y ∂μ) ≠ ∞ := by
convert h'f using 1
apply lintegral_congr_ae
exact hf.ae_eq_mk.symm
filter_upwards [v.ae_tendsto_lintegral_div' hf.measurable_mk A, hf.ae_eq_mk] with x hx h'x
rw [h'x]
convert hx using 1
ext1 a
congr 1
apply lintegral_congr_ae
exact ae_restrict_of_ae hf.ae_eq_mk
