OAI/Analysis/BoundedHochschild/PaulsenExtension.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Extend the two-by-two operator-system map into operators on the doubled Hilbert space, using the proved positive extension theorem.

  1. abbrev OAI.BoundedHochschild.KadisonRingrose.HilbertDouble line 20
  2. abbrev OAI.BoundedHochschild.KadisonRingrose.doubleMatrixHom line 23
  3. lemma OAI.BoundedHochschild.KadisonRingrose.matrixDouble_one line 27
  4. def OAI.BoundedHochschild.KadisonRingrose.paulsenOperatorMap line 33
  5. lemma OAI.BoundedHochschild.KadisonRingrose.paulsenOperatorMap_one line 39
  6. lemma OAI.BoundedHochschild.KadisonRingrose.paulsenOperatorMap_positive line 48
  7. theorem OAI.BoundedHochschild.KadisonRingrose.exists_paulsen_extension line 56