English
For a sequence of nonnegative measurable functions f_n, the liminf of integrals is at least the integral of the liminf: ∫ liminf f_n ≤ liminf ∫ f_n.
Русский
Для последовательности неотрицательных измеримых функций выполняется неравенство Фату: интеграл предела понижающейся последовательности не превышает предел интегралов.
LaTeX
$$$$ \\int^{\\!-}_{a} \\liminf_{n\\to\\infty} f_n(a) \\; d\\mu(a) \\le \\liminf_{n\\to\\infty} \\int^{\\!-}_{a} f_n(a) \\, d\\mu(a). $$$$
Lean4
/-- **Fatou's lemma**, version with `AEMeasurable` functions. -/
theorem lintegral_liminf_le' {f : ℕ → α → ℝ≥0∞} (h_meas : ∀ n, AEMeasurable (f n) μ) :
∫⁻ a, liminf (fun n => f n a) atTop ∂μ ≤ liminf (fun n => ∫⁻ a, f n a ∂μ) atTop :=
calc
∫⁻ a, liminf (fun n => f n a) atTop ∂μ = ∫⁻ a, ⨆ n : ℕ, ⨅ i ≥ n, f i a ∂μ := by
simp only [liminf_eq_iSup_iInf_of_nat]
_ = ⨆ n : ℕ, ∫⁻ a, ⨅ i ≥ n, f i a ∂μ :=
(lintegral_iSup' (fun _ => .biInf _ (to_countable _) (fun i _ ↦ h_meas i))
(ae_of_all μ fun _ _ _ hnm => iInf_le_iInf_of_subset fun _ hi => le_trans hnm hi))
_ ≤ ⨆ n : ℕ, ⨅ i ≥ n, ∫⁻ a, f i a ∂μ := (iSup_mono fun _ => le_iInf₂_lintegral _)
_ = atTop.liminf fun n => ∫⁻ a, f n a ∂μ := Filter.liminf_eq_iSup_iInf_of_nat.symm
