Passing nonnegative integral bounds to an almost-everywhere limit #
theorem
CKN.integral_le_of_ae_tendsto_nonneg
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{f : ℕ → α → ℝ}
{g : α → ℝ}
{bounds : ℕ → ℝ}
{bound : ℝ}
(hf : ∀ (n : ℕ), MeasureTheory.Integrable (f n) μ)
(hfn : ∀ (n : ℕ), 0 ≤ᵐ[μ] f n)
(hg : 0 ≤ᵐ[μ] g)
(hlimit : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x)))
(hbound : 0 ≤ bound)
(hboundLimit : Filter.Tendsto bounds Filter.atTop (nhds bound))
(hupper : ∀ (n : ℕ), ∫ (x : α), f n x ∂μ ≤ bounds n)
:
Fatou's lemma transfers convergent upper bounds on nonnegative integrals.