English
For f: α → ENNReal that is integrable (or has finite integral), for μ-almost every x, the normalized Lintegral of f over a shrinks to f(x) as a shrinks along a Vitali family.
Русский
Для функции f: α → ENNReal интегрируемой (или с конечным интегралом) почти везде верно: нормированная линегральная интеграл по a становится равной f(x) при a уменьшается к x вдоль Vitali.
LaTeX
$$$\forall^{\mu}\ x,\ Tendsto\bigl(\lambda a.\dfrac{\int_{y∈a} f(y)\,dμ}{μ(a)}\bigr)(v.filterAt x)\bigl(\mathcal{N}(f(x))\bigr).$$$
Lean4
theorem ae_tendsto_lintegral_div' {f : α → ℝ≥0∞} (hf : Measurable f) (h'f : (∫⁻ y, f y ∂μ) ≠ ∞) :
∀ᵐ x ∂μ, Tendsto (fun a => (∫⁻ y in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (f x)) :=
by
let ρ := μ.withDensity f
have : IsFiniteMeasure ρ := isFiniteMeasure_withDensity h'f
filter_upwards [ae_tendsto_rnDeriv v ρ, rnDeriv_withDensity μ hf] with x hx h'x
rw [← h'x]
apply hx.congr' _
filter_upwards [v.eventually_filterAt_measurableSet x] with a ha
rw [← withDensity_apply f ha]
