English
Various variants of Fatou’s lemma for nonnegative sequences show liminf of integrals is bounded below by the integral of liminf, in extended real-valued setting.
Русский
Различные формулировки леммы Фату для неотрицательных последовательностей: liminf интегралов не меньше интеграла liminf.
LaTeX
$$$$ \\liminf_{n} \\int f_n \\, d\\mu \\le \\int \\liminf_{n} f_n \\, d\\mu. $$$$
Lean4
theorem lintegral_add_aux {f g : α → ℝ≥0∞} (hf : Measurable f) (hg : Measurable g) :
∫⁻ a, f a + g a ∂μ = ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ :=
calc
∫⁻ a, f a + g a ∂μ = ∫⁻ a, (⨆ n, (eapprox f n : α → ℝ≥0∞) a) + ⨆ n, (eapprox g n : α → ℝ≥0∞) a ∂μ := by
simp only [iSup_eapprox_apply, hf, hg]
_ = ∫⁻ a, ⨆ n, (eapprox f n + eapprox g n : α → ℝ≥0∞) a ∂μ :=
by
congr; funext a
rw [ENNReal.iSup_add_iSup_of_monotone]
· simp only [Pi.add_apply]
· intro i j h
exact monotone_eapprox _ h a
· intro i j h
exact monotone_eapprox _ h a
_ = ⨆ n, (eapprox f n).lintegral μ + (eapprox g n).lintegral μ :=
by
rw [lintegral_iSup]
· congr
funext n
rw [← SimpleFunc.add_lintegral, ← SimpleFunc.lintegral_eq_lintegral]
simp only [Pi.add_apply, SimpleFunc.coe_add]
· fun_prop
· intro i j h a
dsimp
gcongr <;> exact monotone_eapprox _ h _
_ = (⨆ n, (eapprox f n).lintegral μ) + ⨆ n, (eapprox g n).lintegral μ := by
refine (ENNReal.iSup_add_iSup_of_monotone ?_ ?_).symm <;>
· intro i j h
exact SimpleFunc.lintegral_mono (monotone_eapprox _ h) le_rfl
_ = ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ := by
rw [lintegral_eq_iSup_eapprox_lintegral hf, lintegral_eq_iSup_eapprox_lintegral hg]
