Theorems · Theorem · functional analysis

MeasureTheory.Lp.completeSpace_lp_of_cauchy_complete_eLpNorm

∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {E : Type u_3}
  [inst : NormedAddCommGroup E] [hp : Fact (1 ≤ p)],
  (∀ (f : ℕ → α → E),
      (∀ (n : ℕ), MeasureTheory.MemLp (f n) p μ) →
        ∀ (B : ℕ → ENNReal),
          ∑' (i : ℕ), B i < ⊤ →
            (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → MeasureTheory.eLpNorm (f n - f m_1) p μ < B N) →
              ∃ f_lim,
                MeasureTheory.MemLp f_lim p μ ∧
                  Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - f_lim) p μ) Filter.atTop (nhds 0)) →
    CompleteSpace ↥(MeasureTheory.Lp E p μ)

Defined in

Mathlib.MeasureTheory.Function.LpSpace.Complete

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupFact