OAI/Analysis/Nuclearity/CPMatrixFunctional.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A completely positive map to a finite matrix algebra defines a positive functional on the matrix amplification. This is the scalar step in finite matrix extension; the positivity calculation is an explicit matrix corner.

  1. def OAI.WeakPureInfiniteness.cpMatrixFunctionalLinear line 18
  2. lemma OAI.WeakPureInfiniteness.cpMatrixFunctionalLinear_apply line 25
  3. lemma OAI.WeakPureInfiniteness.matrixUnit_corner_product line 30
  4. lemma OAI.WeakPureInfiniteness.cpMatrixFunctionalLinear_nonneg line 38
  5. def OAI.WeakPureInfiniteness.cpMatrixFunctional line 50
  6. lemma OAI.WeakPureInfiniteness.cpMatrixFunctional_apply line 55