theorem fatou_lemma {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} (hf : ∀ (n : ℕ), Measurable (f n)) : ∫⁻ (a : α), Filter.liminf (fun (n : ℕ) => f n a) Filter.atTop ∂μ ≤ Filter.liminf (fun (n : ℕ) => ∫⁻ (a : α), f n a ∂μ) Filter.atTop

Fatou's lemma. For a sequence of nonnegative (ENNReal-valued) measurable functions f n, the integral of the pointwise liminf is bounded above by the liminf of the integrals: ∫ liminf f_n dμ ≤ liminf ∫ f_n dμ.

theorem fatou_lemma' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} (hf : ∀ (n : ℕ), AEMeasurable (f n) μ) : ∫⁻ (a : α), Filter.liminf (fun (n : ℕ) => f n a) Filter.atTop ∂μ ≤ Filter.liminf (fun (n : ℕ) => ∫⁻ (a : α), f n a ∂μ) Filter.atTop

Fatou's lemma (almost-everywhere measurable version). Same statement as fatou_lemma, but only requires each f n to be AEMeasurable rather than Measurable.