English
Lebesgue dominated convergence yields convergence of setToFun when fs n → f a.e., with domination by a bound and integrability of bound and limit function.
Русский
Сходимость Доминированная теорема Лебега применима к сходованию setToFun, когда fs n сходится к f а.е. при господствовании ограничением и интегрируемостью bound.
LaTeX
$$$\\operatorname{tendsto}\\_{n\\to\\infty} \\{ setToFun \\}$$$
Lean4
/-- Lebesgue dominated convergence theorem provides sufficient conditions under which almost
everywhere convergence of a sequence of functions implies the convergence of their image by
`setToFun`.
We could weaken the condition `bound_integrable` to require `HasFiniteIntegral bound μ` instead
(i.e. not requiring that `bound` is measurable), but in all applications proving integrability
is easier. -/
theorem tendsto_setToFun_of_dominated_convergence (hT : DominatedFinMeasAdditive μ T C) {fs : ℕ → α → E} {f : α → E}
(bound : α → ℝ) (fs_measurable : ∀ n, AEStronglyMeasurable (fs n) μ) (bound_integrable : Integrable bound μ)
(h_bound : ∀ n, ∀ᵐ a ∂μ, ‖fs n a‖ ≤ bound a) (h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => fs n a) atTop (𝓝 (f a))) :
Tendsto (fun n => setToFun μ T hT (fs n)) atTop (𝓝 <| setToFun μ T hT f) := by
-- `f` is a.e.-measurable, since it is the a.e.-pointwise limit of a.e.-measurable functions.
have f_measurable : AEStronglyMeasurable f μ := aestronglyMeasurable_of_tendsto_ae _ fs_measurable h_lim
have fs_int : ∀ n, Integrable (fs n) μ := fun n => bound_integrable.mono' (fs_measurable n) (h_bound _)
have f_int : Integrable f μ :=
⟨f_measurable, hasFiniteIntegral_of_dominated_convergence bound_integrable.hasFiniteIntegral h_bound h_lim⟩
-- it suffices to prove the result for the corresponding L1 functions
suffices Tendsto (fun n => L1.setToL1 hT ((fs_int n).toL1 (fs n))) atTop (𝓝 (L1.setToL1 hT (f_int.toL1 f)))
by
convert this with n
· exact setToFun_eq hT (fs_int n)
· exact setToFun_eq hT f_int
refine
L1.tendsto_setToL1 hT _ _
?_
-- up to some rewriting, what we need to prove is `h_lim`
rw [tendsto_iff_norm_sub_tendsto_zero]
have lintegral_norm_tendsto_zero :
Tendsto (fun n => ENNReal.toReal <| ∫⁻ a, ENNReal.ofReal ‖fs n a - f a‖ ∂μ) atTop (𝓝 0) :=
(tendsto_toReal zero_ne_top).comp
(tendsto_lintegral_norm_of_dominated_convergence fs_measurable bound_integrable.hasFiniteIntegral h_bound h_lim)
convert lintegral_norm_tendsto_zero with n
rw [L1.norm_def]
congr 1
refine lintegral_congr_ae ?_
rw [← Integrable.toL1_sub]
refine ((fs_int n).sub f_int).coeFn_toL1.mono fun x hx => ?_
dsimp only
rw [hx, ofReal_norm_eq_enorm, Pi.sub_apply]
