OAI/Analysis/Commutator/CornerAlphabetGNS.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.MatrixCorners.stageAlphabet line 26
  2. lemma OAI.Kadison.MatrixCorners.stageAlphabet_star_mul line 29
  3. lemma OAI.Kadison.MatrixCorners.stageAlphabet_support line 33
  4. lemma OAI.Kadison.MatrixCorners.stageAlphabet_centered line 38
  5. lemma OAI.Kadison.MatrixCorners.stageAlphabet_gram line 43
  6. lemma OAI.Kadison.MatrixCorners.stageAlphabet_norm_le line 52
  7. def OAI.Kadison.MatrixCorners.normalizedStageAlphabet line 60
  8. lemma OAI.Kadison.MatrixCorners.normalization_sq line 63
  9. lemma OAI.Kadison.MatrixCorners.normalizedStageAlphabet_orthonormal line 67
  10. lemma OAI.Kadison.MatrixCorners.normalizedStageAlphabet_norm_le line 79
  11. lemma OAI.Kadison.MatrixCorners.normalizedStageAlphabet_star_mul line 87
  12. lemma OAI.Kadison.MatrixCorners.normalizedStageAlphabet_support line 94
  13. lemma OAI.Kadison.MatrixCorners.normalizedStageAlphabet_centered line 100
  14. lemma OAI.Kadison.MatrixCorners.projection_rank line 106
  15. theorem OAI.Kadison.MatrixCorners.exists_normalized_corner_alphabet line 115