English
Nonnegative measurable functions satisfying a dominating bound converge in the sense of lintegral to the limit function's integral.
Русский
Для неотрицательных измеримых функций с доминирующим пределом интегралы сходятся к интегралу предельной функции.
LaTeX
$$tendsto (∫ f_n) → ∫ f$$
Lean4
/-- **Dominated convergence theorem** for nonnegative `Measurable` functions. -/
theorem tendsto_lintegral_of_dominated_convergence {F : ℕ → α → ℝ≥0∞} {f : α → ℝ≥0∞} (bound : α → ℝ≥0∞)
(hF_meas : ∀ n, Measurable (F n)) (h_bound : ∀ n, F n ≤ᵐ[μ] bound) (h_fin : ∫⁻ 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 ∂μ)) :=
tendsto_of_le_liminf_of_limsup_le
(calc
∫⁻ a, f a ∂μ = ∫⁻ a, liminf (fun n : ℕ => F n a) atTop ∂μ :=
lintegral_congr_ae <| h_lim.mono fun _ h => h.liminf_eq.symm
_ ≤ liminf (fun n => ∫⁻ a, F n a ∂μ) atTop := lintegral_liminf_le hF_meas)
(calc
limsup (fun n : ℕ => ∫⁻ a, F n a ∂μ) atTop ≤ ∫⁻ a, limsup (fun n => F n a) atTop ∂μ :=
limsup_lintegral_le _ hF_meas h_bound h_fin
_ = ∫⁻ a, f a ∂μ := lintegral_congr_ae <| h_lim.mono fun _ h => h.limsup_eq)
