OAI/Analysis/Nuclearity/CommutingMatrixPositive.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Positive matrix coefficients from commuting completely positive and homomorphic ranges. This constructs the finite matrix tensor functional; positivity is proved by the actual Choi square-root coefficients.

  1. lemma OAI.WeakPureInfiniteness.matrix_quadratic_nonneg line 22
  2. def OAI.WeakPureInfiniteness.commutingMatrixLinearMap line 40
  3. lemma OAI.WeakPureInfiniteness.commutingMatrixLinearMap_apply line 50
  4. theorem OAI.WeakPureInfiniteness.commutingMatrixLinearMap_nonneg line 55