OAI/Analysis/BoundedHochschild/FinitePositiveExtension.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The finite-dimensional operator-valued positive extension theorem. Only positivity at the target matrix size is needed.

  1. def OAI.BoundedHochschild.KadisonRingrose.operatorSystemSingle line 17
  2. lemma OAI.BoundedHochschild.KadisonRingrose.operatorSystemSingle_amplification line 26
  3. lemma OAI.BoundedHochschild.KadisonRingrose.operatorSystemMatrixFunctional_single line 48
  4. lemma OAI.BoundedHochschild.KadisonRingrose.euclideanOperator_ext line 71
  5. theorem OAI.BoundedHochschild.KadisonRingrose.exists_finite_completelyPositive_extension line 87