OAI/Analysis/OInfinity/TensorGram.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Matrix-valued Gram return maps for the O∞ tensor approximation

The corner formulation also works in a nonunital tensor completion: the common initial projection need only act identically on the matrix coefficients.

  1. def OAI.WeakPureInfiniteness.supportedCuntzMatrixLinear line 22
  2. lemma OAI.WeakPureInfiniteness.supportedCuntzMatrix_term_mul line 32
  3. def OAI.WeakPureInfiniteness.supportedCuntzMatrixHom line 47
  4. lemma OAI.WeakPureInfiniteness.supportedCuntzMatrixHom_apply line 77
  5. lemma OAI.WeakPureInfiniteness.supportedCuntzMatrixHom_entry line 83
  6. lemma OAI.WeakPureInfiniteness.supportedCuntzMatrixHom_injective line 102
  7. lemma OAI.WeakPureInfiniteness.supportedCuntz_rangeProjection line 115
  8. lemma OAI.WeakPureInfiniteness.supportedCuntzMatrixHom_of_entries line 133
  9. lemma OAI.WeakPureInfiniteness.supportedCuntz_compression_norm_le line 149
  10. lemma OAI.WeakPureInfiniteness.supportedCuntz_gram_apply line 166
  11. lemma OAI.WeakPureInfiniteness.supportedCuntz_gram_norm_le line 194