OAI/Analysis/BoundedHochschild/MatrixFunctionalDilation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A positive functional on a matrix algebra gives a completely positive map into the corresponding finite-dimensional operator algebra.

  1. def OAI.BoundedHochschild.KadisonRingrose.singleCStarMatrix line 18
  2. lemma OAI.BoundedHochschild.KadisonRingrose.singleCStarMatrix_star line 22
  3. lemma OAI.BoundedHochschild.KadisonRingrose.singleCStarMatrix_diagonal line 27
  4. def OAI.BoundedHochschild.KadisonRingrose.matrixFunctionalVector line 37
  5. def OAI.BoundedHochschild.KadisonRingrose.matrixFunctionalEmbedding line 41
  6. lemma OAI.BoundedHochschild.KadisonRingrose.matrixFunctionalEmbedding_single line 48
  7. def OAI.BoundedHochschild.KadisonRingrose.matrixFunctionalCP line 55
  8. lemma OAI.BoundedHochschild.KadisonRingrose.matrixFunctionalCP_coefficient line 62