OAI/Combinatorics/PerfectMatching/Completion.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryMatching.Algorithm.edgeWeight line 11
  2. def OAI.BinaryMatching.Algorithm.matchingWeight line 12
  3. def OAI.BinaryMatching.Algorithm.validMatching line 15
  4. def OAI.BinaryMatching.Algorithm.goodWeight line 18
  5. def OAI.BinaryMatching.Algorithm.badWeight line 21
  6. def OAI.BinaryMatching.Algorithm.Zgood line 24
  7. def OAI.BinaryMatching.Algorithm.Zbad line 25
  8. def OAI.BinaryMatching.Algorithm.multProduct line 27
  9. lemma OAI.BinaryMatching.Algorithm.matchingWeight_exp line 30
  10. lemma OAI.BinaryMatching.Algorithm.matchingWeight_pos line 35
  11. lemma OAI.BinaryMatching.Algorithm.Z_decompose line 38
  12. lemma OAI.BinaryMatching.Algorithm.goodWeight_nonneg line 46
  13. lemma OAI.BinaryMatching.Algorithm.badWeight_nonneg line 51
  14. lemma OAI.BinaryMatching.Algorithm.Zgood_nonneg line 56
  15. lemma OAI.BinaryMatching.Algorithm.Zbad_nonneg line 57
  16. lemma OAI.BinaryMatching.Algorithm.edgeWeight_present line 59
  17. lemma OAI.BinaryMatching.Algorithm.edgeWeight_rounding line 64
  18. lemma OAI.BinaryMatching.Algorithm.invalid_product_zero line 74
  19. lemma OAI.BinaryMatching.Algorithm.goodWeight_le_product line 83
  20. lemma OAI.BinaryMatching.Algorithm.goodWeight_ge_product line 93
  21. lemma OAI.BinaryMatching.Algorithm.Zgood_bracket line 105
  22. lemma OAI.BinaryMatching.Algorithm.positive_count_valid line 116
  23. lemma OAI.BinaryMatching.Algorithm.validWeight_ge_one line 125
  24. lemma OAI.BinaryMatching.Algorithm.Zgood_ge_one line 133
  25. lemma OAI.BinaryMatching.Algorithm.beta_le_B line 138
  26. lemma OAI.BinaryMatching.Algorithm.matching_card_bound line 147
  27. lemma OAI.BinaryMatching.Algorithm.badWeight_bound line 153
  28. lemma OAI.BinaryMatching.Algorithm.Zbad_bound line 176
  29. lemma OAI.BinaryMatching.Algorithm.completion_parameter_bound line 192
  30. lemma OAI.BinaryMatching.Algorithm.Zbad_small line 210
  31. theorem OAI.BinaryMatching.Algorithm.completion_bracket line 222