OAI/Analysis/Nuclearity/CommutingChoiFactor.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Choi square-root coefficients preserve an external commutant. This is the finite matrix positivity step for the commuting tensor functional in KR02 7.18.

  1. lemma OAI.WeakPureInfiniteness.matrix_commute_diagonal_iff line 19
  2. theorem OAI.WeakPureInfiniteness.completelyPositive_matrix_gram_commuting line 37