lintegral_liminf_le — Mathlib

English

Let f_n be nonnegative measurable and Tendsto f_n(a) to F(a) almost everywhere. Then the liminf inequality holds in integral form.

Русский

Пусть f_n неотрицательны и измеримы, и f_n(a) сходится к F(a) почти везде. Тогда верно неравенство Фату в форме интегралов.

LaTeX

$$$$ \\int^{\\!-}_{a} \\liminf_{n} f_n(a) \\; d\\mu(a) \\le \\liminf_{n} \\int^{\\!-}_{a} f_n(a) \\; d\\mu(a). $$$$

Lean4

/-- **Fatou's lemma**, version with `Measurable` functions. -/
theorem lintegral_liminf_le {f : ℕ → α → ℝ≥0∞} (h_meas : ∀ n, Measurable (f n)) :
    ∫⁻ a, liminf (fun n => f n a) atTop ∂μ ≤ liminf (fun n => ∫⁻ a, f n a ∂μ) atTop :=
  lintegral_liminf_le' fun n => (h_meas n).aemeasurable

Похожие утверждения