English
Dominated convergence for sequences of functions with a countable basis filter: convergence of integrals follows from pointwise convergence and domination.
Русский
С теорией доминированного сходимости через фильтры для последовательностей функций: предел интегралов следует из покомпонентного сходства и доминации.
LaTeX
$$$\\lim_{n\\to \\infty} \\int F_n = \\int \\lim F_n$ under domination and countable basis$$
Lean4
/-- Lebesgue dominated convergence theorem for filters with a countable basis -/
theorem tendsto_integral_filter_of_dominated_convergence {ι} {l : Filter ι} [l.IsCountablyGenerated] {F : ι → α → G}
{f : α → G} (bound : α → ℝ) (hF_meas : ∀ᶠ n in l, AEStronglyMeasurable (F n) μ)
(h_bound : ∀ᶠ n in l, ∀ᵐ a ∂μ, ‖F n a‖ ≤ bound a) (bound_integrable : Integrable bound μ)
(h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))) : Tendsto (fun n => ∫ a, F n a ∂μ) l (𝓝 <| ∫ a, f a ∂μ) :=
by
by_cases hG : CompleteSpace G
· simp only [integral, hG, L1.integral]
exact
tendsto_setToFun_filter_of_dominated_convergence (dominatedFinMeasAdditive_weightedSMul μ) bound hF_meas h_bound
bound_integrable h_lim
· simp [integral, hG, tendsto_const_nhds]
