Theorems · Theorem · functional analysis

MeasureTheory.Lp.memLp_of_cauchy_tendsto

∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {E : Type u_3}
  [inst : NormedAddCommGroup E],
  1 ≤ p →
    ∀ {f : ℕ → α → E},
      (∀ (n : ℕ), MeasureTheory.MemLp (f n) p μ) →
        ∀ (f_lim : α → E),
          MeasureTheory.AEStronglyMeasurable f_lim μ →
            Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - f_lim) p μ) Filter.atTop (nhds 0) →
              MeasureTheory.MemLp f_lim p μ

Defined in

Mathlib.MeasureTheory.Function.LpSpace.Complete

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroup