English
Under dominated convergence, the lintegral of the norm tends to 0: Tendsto (∫⁻ ‖F_n - f‖) atTop (nhds 0).
Русский
При доминированном сходящемся пределе интеграл нормы сходится к 0: Tendsto ∫ ‖F_n - f‖ → 0.
LaTeX
$$$\text{tendsto } (n \mapsto \int⁻ a, \|F_n a - f a\| \, ∂μ)\; atTop \; (nhds 0)$$$
Lean4
theorem hasFiniteIntegral_of_dominated_convergence (bound_hasFiniteIntegral : HasFiniteIntegral bound μ)
(h_bound : ∀ n, ∀ᵐ a ∂μ, ‖F n a‖ ≤ bound a) (h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))) :
HasFiniteIntegral f μ := by
/- `‖F n a‖ ≤ bound a` and `‖F n a‖ --> ‖f a‖` implies `‖f a‖ ≤ bound a`,
and so `∫ ‖f‖ ≤ ∫ bound < ∞` since `bound` is has_finite_integral -/
rw [hasFiniteIntegral_iff_norm]
calc
(∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ) ≤ ∫⁻ a, ENNReal.ofReal (bound a) ∂μ :=
lintegral_mono_ae <| all_ae_ofReal_f_le_bound h_bound h_lim
_ < ∞ := by
rw [← hasFiniteIntegral_iff_ofReal]
· exact bound_hasFiniteIntegral
exact (h_bound 0).mono fun a h => le_trans (norm_nonneg _) h
