OAI/Analysis/KadisonKastler/OrderedWordRows.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Creation rows and annihilation columns indexed by ordered labels

  1. def OAI.KadisonKastler.FreeDiagonalModel.creationWord line 24
  2. def OAI.KadisonKastler.FreeDiagonalModel.annihilationWord line 27
  3. theorem OAI.KadisonKastler.FreeDiagonalModel.norm_creationWord_row_le line 30
  4. theorem OAI.KadisonKastler.FreeDiagonalModel.norm_annihilationWord_column_le line 38
  5. theorem OAI.KadisonKastler.FreeDiagonalModel.norm_creationWord_row_le_inv_sqrt line 50
  6. theorem OAI.KadisonKastler.FreeDiagonalModel.norm_annihilationWord_column_le_inv_sqrt line 56
  7. theorem OAI.KadisonKastler.norm_row_matrix_column_entry_le line 64