OAI/Analysis/KadisonKastler/TracialQuotientCompleteness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Two-norm completeness on bounded sets of the tracial quotient

  1. theorem OAI.KadisonKastler.tracialQuotient_bounded_complete line 26

    Source documentation

    Every operator-norm-bounded two-Cauchy sequence has its GNS limit in this quotient. A one-unit norm slack suffices for the subsequent closure proof.

    theorem tracialQuotient_bounded_complete (hω : (ω : Filter ℕ) ≤ atTop)
    (a : ℕ → Q) (C : ℝ) (hC : 0 ≤ C) (ha : ∀ n, ‖a n‖ ≤ C)
    (hc : CauchySeq (fun n => traceStateVector φ (a n))) :
    ∃ b : Q, ‖b‖ ≤ C + 1 ∧
      Tendsto (fun n => traceStateVector φ (a n)) atTop (𝓝 (traceStateVector φ b)) := by
…

    Mentions: OAI.KadisonKastler.traceStateVector