OAI/Analysis/Pureness/Completion/CompletedSourceIncrements.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzPureness.completedDiagonalSum line 10
  2. lemma OAI.CuntzPureness.completedDiagonalSum_nonneg line 13
  3. lemma OAI.CuntzPureness.completedDiagonalSum_mono line 17
  4. lemma OAI.CuntzPureness.matrix_diagonalSum_corner line 25
  5. lemma OAI.CuntzPureness.completedDiagonalSum_monotone line 30
  6. lemma OAI.CuntzPureness.trace_completedDiagonalSum line 42
  7. def OAI.CuntzPureness.completedSourceU line 46
  8. lemma OAI.CuntzPureness.completedSourceU_nonneg line 50
  9. lemma OAI.CuntzPureness.completedSourceU_monotone line 55
  10. lemma OAI.CuntzPureness.completedSourceU_trace_le line 64
  11. theorem OAI.CuntzPureness.completedSourceU_trace_iSup line 73
  12. theorem OAI.CuntzPureness.completedSourceU_trace_tendsto line 90
  13. theorem OAI.CuntzPureness.completedSourceU_increment_nonneg line 99