English
Let f be integrable and measurable, s a set with separable closure. Then the integrals of the approximate-on functions converge to the integral of f as the approximation gets finer.
Русский
Пределы интегралов через’approxOn сходятся к интегралу функции f при улучшении аппроксимации.
LaTeX
$$$\\text{If }f\\text{ is integrable and measurable }s\\text{ separable, then }\\lim_{n\\to\\infty} (\\approxOn(f,s,0,n)\\text{ integral}) = \\int f$.$$
Lean4
theorem tendsto_integral_approxOn_of_measurable [MeasurableSpace E] [BorelSpace E] {f : α → E} {s : Set E}
[SeparableSpace s] (hfi : Integrable f μ) (hfm : Measurable f) (hs : ∀ᵐ x ∂μ, f x ∈ closure s) {y₀ : E}
(h₀ : y₀ ∈ s) (h₀i : Integrable (fun _ => y₀) μ) :
Tendsto (fun n => (SimpleFunc.approxOn f hfm s y₀ h₀ n).integral μ) atTop (𝓝 <| ∫ x, f x ∂μ) :=
by
have hfi' := SimpleFunc.integrable_approxOn hfm hfi h₀ h₀i
simp only [SimpleFunc.integral_eq_integral _ (hfi' _), integral, hE, L1.integral]
exact tendsto_setToFun_approxOn_of_measurable (dominatedFinMeasAdditive_weightedSMul μ) hfi hfm hs h₀ h₀i
