OAI/Analysis/Pureness/Completion/CompletedBlockSeries.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzPureness.completedBlockHom line 10
  2. lemma OAI.CuntzPureness.completedBlock_isometry line 13
  3. lemma OAI.CuntzPureness.completedBlock_norm line 18
  4. lemma OAI.CuntzPureness.completedBlock_nonneg line 23
  5. lemma OAI.CuntzPureness.completedBlock_weight line 29
  6. lemma OAI.CuntzPureness.completedBlock_rank line 36
  7. lemma OAI.CuntzPureness.completedBlock_eq_include line 44
  8. lemma OAI.CuntzPureness.completedBlock_disjoint line 49
  9. def OAI.CuntzPureness.blockStart line 57
  10. lemma OAI.CuntzPureness.blockStart_succ line 59
  11. lemma OAI.CuntzPureness.blockStart_monotone line 62
  12. def OAI.CuntzPureness.completedBlockTerm line 68
  13. lemma OAI.CuntzPureness.completedBlockTerm_orthogonal line 71
  14. theorem OAI.CuntzPureness.exists_completedBlockSum line 84