English
Lebesgue dominated convergence for parameter-dependent interval integrals: under domination and measurability assumptions on F(n, t), the integrals converge to the integral of the limit function as n varies, over intervals a..b.
Русский
Теорема доминированного сходжения Лебега для параметрически-зависимых интегралов по интервалу: при наличии доминирования и меряемости функций F(n, t) интегралы сходятся к интегралу предела.
LaTeX
$$$\\text{HasSum}\\left(\\lambda n, \\int_{a}^{b} F_n(t) \\,dμ(t)\\right) = \\int_{a}^{b} f(t) \\,dμ(t)$$$
Lean4
/-- Lebesgue dominated convergence theorem for parametric interval integrals. -/
nonrec theorem hasSum_integral_of_dominated_convergence {ι} [Countable ι] {F : ι → ℝ → E} (bound : ι → ℝ → ℝ)
(hF_meas : ∀ n, AEStronglyMeasurable (F n) (μ.restrict (Ι a b)))
(h_bound : ∀ n, ∀ᵐ t ∂μ, t ∈ Ι a b → ‖F n t‖ ≤ bound n t)
(bound_summable : ∀ᵐ t ∂μ, t ∈ Ι a b → Summable fun n => bound n t)
(bound_integrable : IntervalIntegrable (fun t => ∑' n, bound n t) μ a b)
(h_lim : ∀ᵐ t ∂μ, t ∈ Ι a b → HasSum (fun n => F n t) (f t)) :
HasSum (fun n => ∫ t in a..b, F n t ∂μ) (∫ t in a..b, f t ∂μ) :=
by
simp only [intervalIntegrable_iff, intervalIntegral_eq_integral_uIoc,
← ae_restrict_iff' (α := ℝ) (μ := μ) measurableSet_uIoc] at *
exact
(hasSum_integral_of_dominated_convergence bound hF_meas h_bound bound_summable bound_integrable h_lim).const_smul _
