OAI/Geometry/TranslativeCovering/MatchingSelf.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingSelf.OffMatching line 34
  2. def OAI.MatchingSelf.off line 37
  3. def OAI.MatchingSelf.available line 46
  4. abbrev OAI.MatchingSelf.Loops line 49
  5. def OAI.MatchingSelf.loops line 51
  6. def OAI.MatchingSelf.join line 64
  7. lemma OAI.MatchingSelf.join_off_loops line 96
  8. lemma OAI.MatchingSelf.off_join line 108
  9. lemma OAI.MatchingSelf.loops_join_val line 120
  10. def OAI.MatchingSelf.splitEquiv line 127
  11. lemma OAI.MatchingSelf.join_product line 137
  12. lemma OAI.MatchingSelf.loop_sum line 147
  13. lemma OAI.MatchingSelf.endpoint_product_le line 164
  14. lemma OAI.MatchingSelf.endpoint_compensation line 173
  15. lemma OAI.MatchingSelf.normalized_term_bound line 207
  16. def OAI.MatchingSelf.leftChoice line 219
  17. lemma OAI.MatchingSelf.leftChoice_eq_some line 222
  18. lemma OAI.MatchingSelf.leftChoice_injective line 233
  19. def OAI.MatchingSelf.rowWeight line 240
  20. lemma OAI.MatchingSelf.row_product line 244
  21. lemma OAI.MatchingSelf.off_sum_le_rows line 270
  22. lemma OAI.MatchingSelf.self_matching_bound line 301