OAI/Analysis/Pureness/Completion/CompletedCompressions.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.CuntzPureness.cornerCompletionOrder line 12
  2. instance OAI.CuntzPureness.cornerCompletionStarOrdered line 13
  3. lemma OAI.CuntzPureness.completedMatrixInclude_nonneg line 15
  4. def OAI.CuntzPureness.completedProjection line 21
  5. lemma OAI.CuntzPureness.completedProjection_star line 23
  6. lemma OAI.CuntzPureness.completedProjection_norm_le line 27
  7. def OAI.CuntzPureness.completedCornerCut line 34
  8. lemma OAI.CuntzPureness.completedCornerCut_continuous line 37
  9. lemma OAI.CuntzPureness.completedCornerCut_sub line 41
  10. lemma OAI.CuntzPureness.completedCornerCut_norm_le line 45
  11. lemma OAI.CuntzPureness.completedCornerCut_fixes line 55
  12. theorem OAI.CuntzPureness.completedCornerCut_tendsto line 62
  13. lemma OAI.CuntzPureness.completedCornerCut_nonneg line 87
  14. lemma OAI.CuntzPureness.completedCornerCut_cuntz line 91