OAI/Analysis/KadisonKastler/CuntzCommutator.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Scalar commutator bounds amplify along commuting Cuntz families

  1. theorem OAI.KadisonKastler.CuntzFamily.assemble_commutator line 26
  2. theorem OAI.KadisonKastler.CuntzFamily.matrix_commutator_le line 56
  3. theorem OAI.KadisonKastler.completelyBounded_commutator_of_commuting_cuntz line 75