OAI/Combinatorics/MatchingCount/Machines/TreeBottleneck.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.TreeFraction.maximum line 9
  2. def OAI.MatchingFPRAS.TreeFraction.minimum line 10
  3. def OAI.MatchingFPRAS.TreeFraction.maximumRealizer line 11
  4. def OAI.MatchingFPRAS.TreeFraction.minimumRealizer line 12
  5. lemma OAI.MatchingFPRAS.TreeFraction.polynomial_maximum line 13
  6. lemma OAI.MatchingFPRAS.TreeFraction.polynomial_minimum line 15
  7. lemma OAI.MatchingFPRAS.TreeFraction.maximum_eq line 17
  8. lemma OAI.MatchingFPRAS.TreeFraction.minimum_eq line 19
  9. lemma OAI.MatchingFPRAS.TreeFraction.maximum_repr line 21
  10. lemma OAI.MatchingFPRAS.TreeFraction.minimum_repr line 29
  11. lemma OAI.MatchingFPRAS.TreeFraction.maximum_weight line 37
  12. lemma OAI.MatchingFPRAS.TreeFraction.minimum_weight line 41
  13. lemma OAI.MatchingFPRAS.TreeFraction.maximum_fold_weight line 45
  14. lemma OAI.MatchingFPRAS.TreeFraction.polynomial_maximumFold line 53
  15. abbrev OAI.MatchingFPRAS.ExecutableBottleneck.Matrix line 65
  16. def OAI.MatchingFPRAS.ExecutableBottleneck.one line 66
  17. def OAI.MatchingFPRAS.ExecutableBottleneck.cell line 67
  18. def OAI.MatchingFPRAS.ExecutableBottleneck.cellRealizer line 68
  19. lemma OAI.MatchingFPRAS.ExecutableBottleneck.polynomial_cell line 70
  20. def OAI.MatchingFPRAS.ExecutableBottleneck.square line 78
  21. def OAI.MatchingFPRAS.ExecutableBottleneck.squareRealizer line 80
  22. lemma OAI.MatchingFPRAS.ExecutableBottleneck.polynomial_square line 86
  23. lemma OAI.MatchingFPRAS.ExecutableBottleneck.cell_weight line 99
  24. def OAI.MatchingFPRAS.ExecutableBottleneck.via line 112
  25. def OAI.MatchingFPRAS.ExecutableBottleneck.viaRealizer line 114
  26. lemma OAI.MatchingFPRAS.ExecutableBottleneck.polynomial_via line 117
  27. def OAI.MatchingFPRAS.ExecutableBottleneck.entry line 128
  28. def OAI.MatchingFPRAS.ExecutableBottleneck.entryRealizer line 131
  29. lemma OAI.MatchingFPRAS.ExecutableBottleneck.polynomial_entry line 136
  30. def OAI.MatchingFPRAS.ExecutableBottleneck.advance line 148
  31. def OAI.MatchingFPRAS.ExecutableBottleneck.advanceRealizer line 149
  32. lemma OAI.MatchingFPRAS.ExecutableBottleneck.polynomial_advance line 150
  33. lemma OAI.MatchingFPRAS.ExecutableBottleneck.advance_length line 152
  34. lemma OAI.MatchingFPRAS.ExecutableBottleneck.entry_weight line 154
  35. lemma OAI.MatchingFPRAS.ExecutableBottleneck.advance_entries line 164
  36. lemma OAI.MatchingFPRAS.ExecutableBottleneck.advance_weight line 170
  37. def OAI.MatchingFPRAS.ExecutableBottleneck.seedEntry line 181
  38. def OAI.MatchingFPRAS.ExecutableBottleneck.seedEntryRealizer line 183
  39. lemma OAI.MatchingFPRAS.ExecutableBottleneck.polynomial_seedEntry line 193
  40. def OAI.MatchingFPRAS.ExecutableBottleneck.seed line 208
  41. def OAI.MatchingFPRAS.ExecutableBottleneck.seedRealizer line 209
  42. lemma OAI.MatchingFPRAS.ExecutableBottleneck.polynomial_seed line 210
  43. def OAI.MatchingFPRAS.ExecutableBottleneck.close line 213
  44. def OAI.MatchingFPRAS.ExecutableBottleneck.closeRealizer line 214
  45. lemma OAI.MatchingFPRAS.ExecutableBottleneck.fold_advance_invariant line 216
  46. lemma OAI.MatchingFPRAS.ExecutableBottleneck.polynomial_closeFold line 242
  47. lemma OAI.MatchingFPRAS.ExecutableBottleneck.polynomial_close line 258