English
A combination of tendsto results for directed families with measurability assumptions and almost everywhere convergence.
Русский
Комбинация пределов для направленных семейств функций с измеримостью и почти то, что сходится.
LaTeX
$$$[Countable] \\Rightarrow ...$$$
Lean4
theorem lintegral_tendsto_of_tendsto_of_antitone {f : ℕ → α → ℝ≥0∞} {F : α → ℝ≥0∞} (hf : ∀ n, AEMeasurable (f n) μ)
(h_anti : ∀ᵐ x ∂μ, Antitone fun n ↦ f n x) (h0 : ∫⁻ a, f 0 a ∂μ ≠ ∞)
(h_tendsto : ∀ᵐ x ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))) :
Tendsto (fun n ↦ ∫⁻ x, f n x ∂μ) atTop (𝓝 (∫⁻ x, F x ∂μ)) :=
by
have : Antitone fun n ↦ ∫⁻ x, f n x ∂μ := fun i j hij ↦ lintegral_mono_ae (h_anti.mono fun x hx ↦ hx hij)
suffices key : ∫⁻ x, F x ∂μ = ⨅ n, ∫⁻ x, f n x ∂μ by
rw [key]
exact tendsto_atTop_iInf this
rw [← lintegral_iInf' hf h_anti h0]
refine lintegral_congr_ae ?_
filter_upwards [h_anti, h_tendsto] with _ hx_anti hx_tendsto using
tendsto_nhds_unique hx_tendsto (tendsto_atTop_iInf hx_anti)
