English
If functions F_n are dominated by an integrable bound and converge pointwise to f, then the integrals converge to the integral of f.
Русский
Если функции F_n доминированы интегрируемым пределом и сходятся точечно к f, то интегралы сходятся к интегралу от f.
LaTeX
$$$\\int f = \\lim_{n}\\int F_n \\quad\\text{under dominating conditions}$$$
Lean4
/-- **Lebesgue dominated convergence theorem** provides sufficient conditions under which almost
everywhere convergence of a sequence of functions implies the convergence of their integrals.
We could weaken the condition `bound_integrable` to require `HasFiniteIntegral bound μ` instead
(i.e. not requiring that `bound` is measurable), but in all applications proving integrability
is easier. -/
theorem tendsto_integral_of_dominated_convergence {F : ℕ → α → G} {f : α → G} (bound : α → ℝ)
(F_measurable : ∀ n, AEStronglyMeasurable (F n) μ) (bound_integrable : Integrable bound μ)
(h_bound : ∀ n, ∀ᵐ a ∂μ, ‖F n a‖ ≤ bound a) (h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))) :
Tendsto (fun n => ∫ a, F n a ∂μ) atTop (𝓝 <| ∫ a, f a ∂μ) :=
by
by_cases hG : CompleteSpace G
· simp only [integral, hG, L1.integral]
exact
tendsto_setToFun_of_dominated_convergence (dominatedFinMeasAdditive_weightedSMul μ) bound F_measurable
bound_integrable h_bound h_lim
· simp [integral, hG]
