Theorems · Theorem · functional analysis

MeasureTheory.Lp.cauchy_tendsto_of_tendsto

∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {E : Type u_3}
  [inst : NormedAddCommGroup E] {f : ℕ → α → E},
  (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
    ∀ (f_lim : α → E) {B : ℕ → ENNReal},
      ∑' (i : ℕ), B i ≠ ⊤ →
        (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → MeasureTheory.eLpNorm (f n - f m_1) p μ < B N) →
          (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (f_lim x))) →
            Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - f_lim) p μ) Filter.atTop (nhds 0)

Defined in

Mathlib.MeasureTheory.Function.LpSpace.Complete

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroup