OAI/Computability/LoopMatching/ExpandInput.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Polynomial-time approximation of weighted matchings with singleton loops.

  1. def OAI.LoopMatching.crossRecord line 10
  2. def OAI.LoopMatching.crossRecords line 13
  3. lemma OAI.LoopMatching.mem_crossRecords line 16
  4. lemma OAI.LoopMatching.crossRecords_length line 20
  5. lemma OAI.LoopMatching.crossRecords_unique line 30
  6. def OAI.LoopMatching.expand line 53
  7. lemma OAI.LoopMatching.expand_n line 81
  8. lemma OAI.LoopMatching.expand_records_length line 83
  9. lemma OAI.LoopMatching.expand_records_length_le line 87
  10. def OAI.LoopMatching.oldPair line 92
  11. def OAI.LoopMatching.crossPair line 97
  12. def OAI.LoopMatching.dummyPair line 105
  13. lemma OAI.LoopMatching.find_some_unique line 113
  14. lemma OAI.LoopMatching.find_cross_block line 122
  15. lemma OAI.LoopMatching.find_crossRecords line 143
  16. lemma OAI.LoopMatching.multiplicity_expand_old line 157
  17. lemma OAI.LoopMatching.multiplicity_expand_cross line 177
  18. lemma OAI.LoopMatching.multiplicity_expand_dummy line 198