Theorems · Theorem · functional analysis

MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNorm

∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : SeminormedAddGroup E] {f : ℕ → α → E},
  (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
    ∀ (f_lim : α → E),
      (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (f_lim x))) →
        MeasureTheory.eLpNorm f_lim p μ ≤ Filter.liminf (fun n => MeasureTheory.eLpNorm (f n) p μ) Filter.atTop

Defined in

Mathlib.MeasureTheory.Function.LpSpace.Complete

Cited by

3 results in Mathlib

Foundations

Depth 211 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedAddGroup