OAI/Analysis/Nuclearity/NuclearCommutingCP.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The positive map on the minimal tensor product defined by a completely positive map and a commuting representation. This is the functional construction needed in KR02 Lemma 7.18, specialized to a nuclear first factor.

  1. def OAI.WeakPureInfiniteness.cpCommutingPolynomial line 24
  2. lemma OAI.WeakPureInfiniteness.cpCommutingPolynomial_bound line 28
  3. def OAI.WeakPureInfiniteness.cpCommutingLinear line 38
  4. lemma OAI.WeakPureInfiniteness.cpCommutingLinear_polynomial line 41
  5. lemma OAI.WeakPureInfiniteness.cpCommutingLinear_elementary line 48
  6. lemma OAI.WeakPureInfiniteness.cpCommutingLinear_polynomial_square_nonneg line 55
  7. lemma OAI.WeakPureInfiniteness.cpCommutingLinear_nonneg line 71
  8. def OAI.WeakPureInfiniteness.cpCommutingPositiveMap line 78