English
A variant of dominated convergence for measurably embedded functions; equality of limits holds under appropriate measurability constraints.
Русский
Вариант доминированной конвергенции для измеримых вложенных функций; при надлежащих условиях измеримости пределы совпадают.
LaTeX
$$limiting behavior of ∫ F_n equals ∫ F$$
Lean4
/-- **Dominated convergence theorem** for nonnegative `AEMeasurable` functions. -/
theorem tendsto_lintegral_of_dominated_convergence' {F : ℕ → α → ℝ≥0∞} {f : α → ℝ≥0∞} (bound : α → ℝ≥0∞)
(hF_meas : ∀ n, AEMeasurable (F n) μ) (h_bound : ∀ n, F n ≤ᵐ[μ] bound) (h_fin : ∫⁻ a, bound a ∂μ ≠ ∞)
(h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))) :
Tendsto (fun n => ∫⁻ a, F n a ∂μ) atTop (𝓝 (∫⁻ a, f a ∂μ)) :=
by
have : ∀ n, ∫⁻ a, F n a ∂μ = ∫⁻ a, (hF_meas n).mk (F n) a ∂μ := fun n => lintegral_congr_ae (hF_meas n).ae_eq_mk
simp_rw [this]
apply tendsto_lintegral_of_dominated_convergence bound (fun n => (hF_meas n).measurable_mk) _ h_fin
· have : ∀ n, ∀ᵐ a ∂μ, (hF_meas n).mk (F n) a = F n a := fun n => (hF_meas n).ae_eq_mk.symm
have : ∀ᵐ a ∂μ, ∀ n, (hF_meas n).mk (F n) a = F n a := ae_all_iff.mpr this
filter_upwards [this, h_lim] with a H H'
simp_rw [H]
exact H'
· intro n
filter_upwards [h_bound n, (hF_meas n).ae_eq_mk] with a H H'
rwa [H'] at H
