English
Let {F_i} be a family of measurable functions indexed by a countable set ι, each bounded by a real-valued bound bound_i(a) such that the bound's sum is integrable almost everywhere, and suppose F_i(a) converges pointwise to f(a) almost everywhere. Then one may interchange the sum and the integral: the series of integrals ∑_i ∫ F_i(a) dμ(a) converges to ∫ f(a) dμ(a).
Русский
Пусть имеется семейство измеримых функций {F_i}, индексируемое счётным множеством ι, каждая из которых ограничена по модулю функцией bound_i(a) так, что сумма bound_i(a) по i интегрируема почти везде по μ, и предположим, что F_i(a) сходится по по точкам к f(a) почти всюду. Тогда можно поменять порядок суммирования и интегрирования: сумма интегралов ∑_i ∫ F_i dμ = ∫ f dμ.
LaTeX
$$$\\text{HasSum}\\left(\\lambda i. \\int_α F_i(a)\\,dμ(a)\\right)\\left(\\int_α f(a)\\,dμ(a)\\right)$$$
Lean4
/-- Lebesgue dominated convergence theorem for series. -/
theorem hasSum_integral_of_dominated_convergence {ι} [Countable ι] {F : ι → α → G} {f : α → G} (bound : ι → α → ℝ)
(hF_meas : ∀ n, AEStronglyMeasurable (F n) μ) (h_bound : ∀ n, ∀ᵐ a ∂μ, ‖F n a‖ ≤ bound n a)
(bound_summable : ∀ᵐ a ∂μ, Summable fun n => bound n a) (bound_integrable : Integrable (fun a => ∑' n, bound n a) μ)
(h_lim : ∀ᵐ a ∂μ, HasSum (fun n => F n a) (f a)) : HasSum (fun n => ∫ a, F n a ∂μ) (∫ a, f a ∂μ) :=
by
have hb_nonneg : ∀ᵐ a ∂μ, ∀ n, 0 ≤ bound n a :=
eventually_countable_forall.2 fun n => (h_bound n).mono fun a => (norm_nonneg _).trans
have hb_le_tsum : ∀ n, bound n ≤ᵐ[μ] fun a => ∑' n, bound n a :=
by
intro n
filter_upwards [hb_nonneg, bound_summable] with _ ha0 ha_sum using ha_sum.le_tsum _ fun i _ => ha0 i
have hF_integrable : ∀ n, Integrable (F n) μ :=
by
refine fun n => bound_integrable.mono' (hF_meas n) ?_
exact EventuallyLE.trans (h_bound n) (hb_le_tsum n)
simp only [HasSum, ← integral_finset_sum _ fun n _ => hF_integrable n]
refine tendsto_integral_filter_of_dominated_convergence (fun a => ∑' n, bound n a) ?_ ?_ bound_integrable h_lim
· exact Eventually.of_forall fun s => s.aestronglyMeasurable_fun_sum fun n _ => hF_meas n
· filter_upwards with s
filter_upwards [eventually_countable_forall.2 h_bound, hb_nonneg, bound_summable] with a hFa ha0 has
calc
‖∑ n ∈ s, F n a‖ ≤ ∑ n ∈ s, bound n a := norm_sum_le_of_le _ fun n _ => hFa n
_ ≤ ∑' n, bound n a := has.sum_le_tsum _ (fun n _ => ha0 n)
