OAI/Analysis/BoundedHochschild/PaulsenMatrixBlocks.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Identify amplified two-by-two operator systems with scalar-diagonal blocks.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.positiveBlock_zero_zero line 18
  2. lemma OAI.BoundedHochschild.KadisonRingrose.positiveBlock_zero_one line 20
  3. lemma OAI.BoundedHochschild.KadisonRingrose.positiveBlock_one_zero line 22
  4. lemma OAI.BoundedHochschild.KadisonRingrose.positiveBlock_one_one line 24
  5. lemma OAI.BoundedHochschild.KadisonRingrose.paulsen_scalar_coefficient line 27
  6. lemma OAI.BoundedHochschild.KadisonRingrose.paulsen_diagonal_coefficient line 31
  7. def OAI.BoundedHochschild.KadisonRingrose.paulsenMatrixDiagonal line 43
  8. def OAI.BoundedHochschild.KadisonRingrose.paulsenMatrixUpper line 47
  9. lemma OAI.BoundedHochschild.KadisonRingrose.paulsenMatrix_lower line 50
  10. lemma OAI.BoundedHochschild.KadisonRingrose.paulsenMatrix_source_block line 55
  11. lemma OAI.BoundedHochschild.KadisonRingrose.paulsenMatrix_target_block line 82