OAI/Analysis/Nuclearity/MatrixCPAmplification.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite matrix amplification of completely positive contractions. Only finite reindexing and the positive matrix norm bound are used.

  1. lemma OAI.WeakPureInfiniteness.sum_cstarMatrix_apply line 17
  2. def OAI.WeakPureInfiniteness.flattenCStarMatrix line 22
  3. def OAI.WeakPureInfiniteness.unflattenCStarMatrix line 37
  4. lemma OAI.WeakPureInfiniteness.unflatten_flattenCStarMatrix line 54
  5. lemma OAI.WeakPureInfiniteness.matrixLinearMap_completelyPositive line 64
  6. lemma OAI.WeakPureInfiniteness.matrixLinearMap_norm_le_one line 79