OAI/Analysis/PureInfiniteness/CuntzGramMap.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Finite matrix return maps from Cuntz families

Conjugating the matrix corner associated to orthogonal isometries realizes the Gram-coefficient maps used by the finite Fock approximation.

  1. def OAI.WeakPureInfiniteness.cuntzMatrixLinear line 19
  2. lemma OAI.WeakPureInfiniteness.cuntzMatrixLinear_apply line 23
  3. lemma OAI.WeakPureInfiniteness.cuntzMatrix_term_mul line 29
  4. def OAI.WeakPureInfiniteness.cuntzMatrixHom line 40
  5. lemma OAI.WeakPureInfiniteness.cuntzMatrixHom_apply line 68
  6. def OAI.WeakPureInfiniteness.cuntzGramMap line 73
  7. lemma OAI.WeakPureInfiniteness.cuntzGramMap_apply line 79
  8. lemma OAI.WeakPureInfiniteness.cuntzGramMap_one line 114
  9. lemma OAI.WeakPureInfiniteness.cuntzGramMap_cp line 122