English
If f_n is an antitone sequence with pointwise Tendsto to F almost everywhere and the initial integral is finite, then the limit of the integrals equals the integral of the limit.
Русский
Если последовательность f_n антитонична почти в каждой точке и сходится к F почти всюду, и начальный интеграл конечен, то предел интегралов равен интегралу предела.
LaTeX
$$$(hf : \\forall n, AEMeasurable (f_n) μ) \\rightarrow (h_{anti} : \\text{Antitone (fun n => f_n x) μ}) \\rightarrow (h0 : ∫⁻ a, f_0 a ∂μ ≠ ∞) \\rightarrow (h_tendsto : ∀ᵐ x ∂μ, Tendsto (fun n => f_n x) atTop (𝓝 (F x))) \\Rightarrow Tendsto (fun n => ∫⁻ x, f_n x ∂μ) atTop (𝓝 (∫⁻ x, F x ∂μ))$$$
Lean4
/-- **Monotone convergence theorem** for nonincreasing sequences of functions. -/
theorem lintegral_iInf_ae {f : ℕ → α → ℝ≥0∞} (h_meas : ∀ n, Measurable (f n)) (h_mono : ∀ n : ℕ, f n.succ ≤ᵐ[μ] f n)
(h_fin : ∫⁻ a, f 0 a ∂μ ≠ ∞) : ∫⁻ a, ⨅ n, f n a ∂μ = ⨅ n, ∫⁻ a, f n a ∂μ :=
have fn_le_f0 : ∫⁻ a, ⨅ n, f n a ∂μ ≤ ∫⁻ a, f 0 a ∂μ := lintegral_mono fun _ => iInf_le_of_le 0 le_rfl
have fn_le_f0' : ⨅ n, ∫⁻ a, f n a ∂μ ≤ ∫⁻ a, f 0 a ∂μ := iInf_le_of_le 0 le_rfl
(ENNReal.sub_right_inj h_fin fn_le_f0 fn_le_f0').1 <|
show ∫⁻ a, f 0 a ∂μ - ∫⁻ a, ⨅ n, f n a ∂μ = ∫⁻ a, f 0 a ∂μ - ⨅ n, ∫⁻ a, f n a ∂μ from
calc
∫⁻ a, f 0 a ∂μ - ∫⁻ a, ⨅ n, f n a ∂μ = ∫⁻ a, f 0 a - ⨅ n, f n a ∂μ :=
(lintegral_sub (.iInf h_meas) (ne_top_of_le_ne_top h_fin <| lintegral_mono fun _ => iInf_le _ _)
(ae_of_all _ fun _ => iInf_le _ _)).symm
_ = ∫⁻ a, ⨆ n, f 0 a - f n a ∂μ := (congr rfl (funext fun _ => ENNReal.sub_iInf))
_ = ⨆ n, ∫⁻ a, f 0 a - f n a ∂μ :=
(lintegral_iSup_ae (fun n => (h_meas 0).sub (h_meas n)) fun n =>
(h_mono n).mono fun _ ha => tsub_le_tsub le_rfl ha)
_ = ⨆ n, ∫⁻ a, f 0 a ∂μ - ∫⁻ a, f n a ∂μ :=
(have h_mono : ∀ᵐ a ∂μ, ∀ n : ℕ, f n.succ a ≤ f n a := ae_all_iff.2 h_mono
have h_mono : ∀ n, ∀ᵐ a ∂μ, f n a ≤ f 0 a := fun n =>
h_mono.mono fun a h => by
induction n with
| zero => rfl
| succ n ih => exact (h n).trans ih
congr_arg iSup <|
funext fun n =>
lintegral_sub (h_meas _) (ne_top_of_le_ne_top h_fin <| lintegral_mono_ae <| h_mono n) (h_mono n))
_ = ∫⁻ a, f 0 a ∂μ - ⨅ n, ∫⁻ a, f n a ∂μ := ENNReal.sub_iInf.symm
