OAI/Analysis/BoundedHochschild/OperatorSystemMatrices.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The scalar matrix functional used in finite-dimensional positive extension.

  1. def OAI.BoundedHochschild.KadisonRingrose.operatorSystemMatrices line 17
  2. lemma OAI.BoundedHochschild.KadisonRingrose.operatorSystemMatrices_one line 25
  3. lemma OAI.BoundedHochschild.KadisonRingrose.operatorSystemMatrices_star line 34
  4. def OAI.BoundedHochschild.KadisonRingrose.operatorSystemAmplification line 39
  5. def OAI.BoundedHochschild.KadisonRingrose.operatorSystemMatrixFunctional line 52
  6. lemma OAI.BoundedHochschild.KadisonRingrose.operatorSystemMatrixFunctional_nonneg line 56