OAI/Analysis/KadisonKastler/TracialQuotientVonNeumann.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The tracial sequence quotient is a represented von Neumann algebra

  1. def OAI.KadisonKastler.tracialSequenceAlgebra line 26
  2. theorem OAI.KadisonKastler.tracialSequenceAlgebra_contraction_in_range line 30

    Source documentation

    A contraction in the bicommutant is recovered by bounded two-completeness.

    theorem tracialSequenceAlgebra_contraction_in_range (hω : (ω : Filter ℕ) ≤ atTop)
    (T : K →L[ℂ] K) (hT : T ∈ tracialSequenceAlgebra τ ω) (hn : ‖T‖ ≤ 1) :
    ∃ b : Q, π b = T := by
…

    Mentions: OAI.KadisonKastler.tracialSequenceAlgebra