OAI/Analysis/KadisonKastler/AsymptoticCentralizer.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The C-star algebra of asymptotically central bounded sequences

The centrality defect is measured on the standard reference vector. Its product estimate and adjoint symmetry give the sequence algebra used in the bicentralizer argument (Haagerup, Acta Math.158(1987), §1).

  1. def OAI.KadisonKastler.AsymptoticallyCentral line 23
  2. theorem OAI.KadisonKastler.AsymptoticallyCentral.add line 27
  3. theorem OAI.KadisonKastler.AsymptoticallyCentral.smul line 36
  4. theorem OAI.KadisonKastler.AsymptoticallyCentral.star line 43
  5. theorem OAI.KadisonKastler.AsymptoticallyCentral.mul line 50
  6. theorem OAI.KadisonKastler.asymptoticallyCentral_isClosed line 62
  7. def OAI.KadisonKastler.centralSequenceAlgebra line 92
  8. theorem OAI.KadisonKastler.centralSequenceAlgebra_isClosed line 111