English
If F_n are norm-bounded by a constant C almost everywhere and converge to f almost everywhere, with μ finite, then the integrals converge: ∫ F_n → ∫ f.
Русский
Если F_n ограничены по норме константой и сходятся к f, то интегралы сходятся: ∫ F_n → ∫ f.
LaTeX
$$$\\lim_{n\\to\\infty} \\int_α F_n(a)\\,dμ(a) = \\int_α f(a)\\,dμ(a)$$$
Lean4
/-- Lebesgue dominated convergence theorem for filters with a countable basis -/
nonrec theorem tendsto_integral_filter_of_dominated_convergence {ι} {l : Filter ι} [l.IsCountablyGenerated]
{F : ι → ℝ → E} (bound : ℝ → ℝ) (hF_meas : ∀ᶠ n in l, AEStronglyMeasurable (F n) (μ.restrict (Ι a b)))
(h_bound : ∀ᶠ n in l, ∀ᵐ x ∂μ, x ∈ Ι a b → ‖F n x‖ ≤ bound x) (bound_integrable : IntervalIntegrable bound μ a b)
(h_lim : ∀ᵐ x ∂μ, x ∈ Ι a b → Tendsto (fun n => F n x) l (𝓝 (f x))) :
Tendsto (fun n => ∫ x in a..b, F n x ∂μ) l (𝓝 <| ∫ x in a..b, f x ∂μ) :=
by
simp only [intervalIntegrable_iff, intervalIntegral_eq_integral_uIoc,
← ae_restrict_iff' (α := ℝ) (μ := μ) measurableSet_uIoc] at *
exact
tendsto_const_nhds.smul <|
tendsto_integral_filter_of_dominated_convergence bound hF_meas h_bound bound_integrable h_lim
