English
If F_n: α → G are bounded in norm by a constant C almost everywhere and converge to f pointwise almost everywhere, and μ is finite, then ∫ F_n dμ → ∫ f dμ as n→∞.
Русский
Если F_n ограничены по норме постоянной C почти где-либо и сходятся к f почти всюду, а мера μ конечна, то интегралы сходятся: ∫ F_n dμ → ∫ f dμ.
LaTeX
$$$\\lim_{n\\to\\infty} \\int_α F_n(a)\\,dμ(a) = \\int_α f(a)\\,dμ(a)$$$
Lean4
/-- Corollary of the Lebesgue dominated convergence theorem: If a sequence of functions `F n` is
(eventually) uniformly bounded by a constant and converges (eventually) pointwise to a
function `f`, then the integrals of `F n` with respect to a finite measure `μ` converge
to the integral of `f`. -/
theorem tendsto_integral_filter_of_norm_le_const {ι} {l : Filter ι} [l.IsCountablyGenerated] {F : ι → α → G}
[IsFiniteMeasure μ] {f : α → G} (h_meas : ∀ᶠ n in l, AEStronglyMeasurable (F n) μ)
(h_bound : ∃ C, ∀ᶠ n in l, (∀ᵐ ω ∂μ, ‖F n ω‖ ≤ C)) (h_lim : ∀ᵐ ω ∂μ, Tendsto (fun n => F n ω) l (𝓝 (f ω))) :
Tendsto (fun n => ∫ ω, F n ω ∂μ) l (nhds (∫ ω, f ω ∂μ)) :=
by
obtain ⟨c, h_boundc⟩ := h_bound
let C : α → ℝ := (fun _ => c)
exact tendsto_integral_filter_of_dominated_convergence C h_meas h_boundc (integrable_const c) h_lim
