OAI/Analysis/Pureness/Completion/CompletedTraceWeight.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CuntzPureness.completedCornerCut_add line 10
  2. lemma OAI.CuntzPureness.completedCornerCut_smul line 14
  3. def OAI.CuntzPureness.completedCompressLinear line 18
  4. lemma OAI.CuntzPureness.completedCompress_mono line 29
  5. lemma OAI.CuntzPureness.completedCompress_include_of_le line 36
  6. def OAI.CuntzPureness.completedTraceValue line 41
  7. def OAI.CuntzPureness.completedDiagonalWeight line 44
  8. lemma OAI.CuntzPureness.completedTraceValue_continuous line 47
  9. lemma OAI.CuntzPureness.completedTraceValue_mono line 52
  10. lemma OAI.CuntzPureness.completedTraceValue_monotone line 57
  11. lemma OAI.CuntzPureness.completedDiagonalWeight_tendsto line 63
  12. lemma OAI.CuntzPureness.completedDiagonalWeight_mono line 67
  13. lemma OAI.CuntzPureness.completedTraceValue_add line 71
  14. theorem OAI.CuntzPureness.completedDiagonalWeight_add line 82
  15. theorem OAI.CuntzPureness.completedDiagonalWeight_include line 90
  16. theorem OAI.CuntzPureness.completedDiagonalWeight_le_of_tendsto line 104