OAI/Analysis/Pureness/Stabilization/MatrixCompression.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzTrace.matrixFamilyMask line 11
  2. lemma OAI.CuntzTrace.matrixFamilyMask_vanishing line 18
  3. def OAI.CuntzTrace.matrixQuotientMask line 23
  4. lemma OAI.CuntzTrace.matrixQuotientMask_mk line 27
  5. lemma OAI.CuntzTrace.matrixQuotientMask_norm_le line 30
  6. def OAI.CuntzTrace.matrixQuotientMaskCLM line 37
  7. lemma OAI.CuntzTrace.matrixQuotientMask_stage line 40
  8. lemma OAI.CuntzTrace.matrixQuotientMask_mem_limit line 48
  9. def OAI.CuntzTrace.matrixCompression line 55
  10. lemma OAI.CuntzTrace.matrixCompression_norm_le line 60
  11. lemma OAI.CuntzTrace.matrixCompression_stage line 63
  12. theorem OAI.CuntzTrace.contractions_tendsto line 67
  13. theorem OAI.CuntzTrace.matrixCompression_tendsto line 84