English
Under dominated convergence, pointwise a.e. convergence of fs_n to f implies Tendsto condExpL1 hm μ (fs_n) to condExpL1 hm μ f.
Русский
При доминированной сходимости, если f_n сходится к f почти всюду, то условные ожидания сходятся по L1.
LaTeX
$$$\text{Tendsto}\_{n\to\infty} \; condExpL1 hm μ (fs_n) \to \; condExpL1 hm μ f$$$
Lean4
/-- **Lebesgue dominated convergence theorem**: sufficient conditions under which almost
everywhere convergence of a sequence of functions implies the convergence of their image by
`condExpL1`. -/
theorem tendsto_condExpL1_of_dominated_convergence (hm : m ≤ m₀) [SigmaFinite (μ.trim hm)] {fs : ℕ → α → E} {f : α → E}
(bound_fs : α → ℝ) (hfs_meas : ∀ n, AEStronglyMeasurable (fs n) μ) (h_int_bound_fs : Integrable bound_fs μ)
(hfs_bound : ∀ n, ∀ᵐ x ∂μ, ‖fs n x‖ ≤ bound_fs x) (hfs : ∀ᵐ x ∂μ, Tendsto (fun n => fs n x) atTop (𝓝 (f x))) :
Tendsto (fun n => condExpL1 hm μ (fs n)) atTop (𝓝 (condExpL1 hm μ f)) :=
tendsto_setToFun_of_dominated_convergence _ bound_fs hfs_meas h_int_bound_fs hfs_bound hfs
