English
Let β be countable and f: β → α → ℝ≥0∞ be measurable in each argument, directed by ≤. Then the integral of the pointwise supremum equals the supremum of the integrals: ∫ a ⨆ b f(b,a) dμ = ⨆ b ∫ a f(b,a) dμ.
Русский
Пусть β счётно, и для каждого b интегрируемо f(b,·). Если f упорядочено направленно, то интеграл по точке суммы равен супреме интегралов.
LaTeX
$$$$ \\int^{\\!-}_{a} \\bigg( \\bigvee_{b} f(b,a) \\bigg) d\\mu(a) = \\bigvee_{b} \\bigg( \\int^{\\!-}_{a} f(b,a) d\\mu(a) \\bigg). $$$$
Lean4
/-- **Monotone convergence theorem** expressed with limits. -/
theorem lintegral_tendsto_of_tendsto_of_monotone {f : ℕ → α → ℝ≥0∞} {F : α → ℝ≥0∞} (hf : ∀ n, AEMeasurable (f n) μ)
(h_mono : ∀ᵐ x ∂μ, Monotone fun n => f n x) (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 : Monotone fun n => ∫⁻ x, f n x ∂μ := fun i j hij => lintegral_mono_ae (h_mono.mono fun x hx => hx hij)
suffices key : ∫⁻ x, F x ∂μ = ⨆ n, ∫⁻ x, f n x ∂μ by
rw [key]
exact tendsto_atTop_iSup this
rw [← lintegral_iSup' hf h_mono]
refine lintegral_congr_ae ?_
filter_upwards [h_mono, h_tendsto] with _ hx_mono hx_tendsto using
tendsto_nhds_unique hx_tendsto (tendsto_atTop_iSup hx_mono)
