Theorems · Theorem · measure theory

MeasureTheory.eLpNorm_le_of_tendstoInMeasure

∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_5}
  [inst : SeminormedAddGroup E] {u : Filter ι} [u.NeBot] [u.IsCountablyGenerated] {f : ι → α → E} {g : α → E}
  {C p : ENNReal},
  (∀ᶠ (i : ι) in u, MeasureTheory.eLpNorm (f i) p μ ≤ C) →
    MeasureTheory.TendstoInMeasure μ f u g →
      (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) → MeasureTheory.eLpNorm g p μ ≤ C

If the eLpNorm of a collection of AEStronglyMeasurable functions that converges in measure is bounded by some constant C, then the eLpNorm of its limit is also bounded by C.

Defined in

Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Cited by

2 results in Mathlib

Foundations

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

Assumes

SeminormedAddGroupFilter.NeBotFilter.IsCountablyGenerated