OAI/Analysis/KadisonKastler/MatrixStrictContraction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Strict diagonal contraction in two-by-two coordinates

  1. def OAI.KadisonKastler.firstBlockProjection line 13
  2. theorem OAI.KadisonKastler.firstBlockProjection_isStarProjection line 15
  3. theorem OAI.KadisonKastler.secondBlockProjection_eq line 25
  4. theorem OAI.KadisonKastler.lowerLeft_column_square line 31
  5. theorem OAI.KadisonKastler.upperRight_column_square line 41
  6. theorem OAI.KadisonKastler.two_corner_diagonal_eq line 51
  7. theorem OAI.KadisonKastler.blockDiagonal_nonneg line 72
  8. theorem OAI.KadisonKastler.blockDiagonal_mono line 85
  9. theorem OAI.KadisonKastler.norm_matrix_diagonal_lt_of_positive_corner line 93