OAI/Combinatorics/MatchingCount/Graphs/EnlargementRun.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.Transport.ladderLaw_pos line 21
  2. lemma OAI.MatchingFPRAS.Transport.ladderWalk_nonneg line 27
  3. lemma OAI.MatchingFPRAS.Transport.ladderWalk_sum line 34
  4. lemma OAI.MatchingFPRAS.Enlargement.revealLaw_nonneg line 59
  5. lemma OAI.MatchingFPRAS.Enlargement.revealLaw_sum line 70
  6. def OAI.MatchingFPRAS.Enlargement.sourceRun line 79
  7. lemma OAI.MatchingFPRAS.Enlargement.sourceRun_nonneg line 88
  8. lemma OAI.MatchingFPRAS.Enlargement.sourceRun_sum line 98
  9. theorem OAI.MatchingFPRAS.Enlargement.sourceRun_tv line 105
  10. structure OAI.MatchingFPRAS.UnitRefresh.Pairing line 122
  11. instance OAI.MatchingFPRAS.UnitRefresh.(instance at line 127) line 127
  12. instance OAI.MatchingFPRAS.UnitRefresh.(instance at line 134) line 134
  13. lemma OAI.MatchingFPRAS.UnitRefresh.Pairing.ext line 136
  14. def OAI.MatchingFPRAS.UnitRefresh.Pairing.map line 143
  15. def OAI.MatchingFPRAS.UnitRefresh.Pairing.congr line 152
  16. lemma OAI.MatchingFPRAS.UnitRefresh.Pairing.subtype_hext line 158
  17. def OAI.MatchingFPRAS.UnitRefresh.Pairing.remove line 170
  18. def OAI.MatchingFPRAS.UnitRefresh.Pairing.insert line 181
  19. lemma OAI.MatchingFPRAS.UnitRefresh.Pairing.insert_at line 201
  20. lemma OAI.MatchingFPRAS.UnitRefresh.Pairing.insert_other line 205
  21. def OAI.MatchingFPRAS.UnitRefresh.Pairing.split line 210
  22. def OAI.MatchingFPRAS.UnitRefresh.pairingCount line 232
  23. lemma OAI.MatchingFPRAS.UnitRefresh.pairingCount_zero line 237
  24. lemma OAI.MatchingFPRAS.UnitRefresh.pairingCount_one line 239
  25. lemma OAI.MatchingFPRAS.UnitRefresh.pairingCount_add_two line 241
  26. lemma OAI.MatchingFPRAS.UnitRefresh.pairingCount_pos_recurrence line 243
  27. lemma OAI.MatchingFPRAS.UnitRefresh.card_except_two line 250
  28. theorem OAI.MatchingFPRAS.UnitRefresh.pairing_card_aux line 261
  29. theorem OAI.MatchingFPRAS.UnitRefresh.pairing_card line 292
  30. def OAI.MatchingFPRAS.Initializer.restrictHoles line 303
  31. def OAI.MatchingFPRAS.Initializer.fillFixed line 309
  32. lemma OAI.MatchingFPRAS.Initializer.fillFixed_holes line 320
  33. def OAI.MatchingFPRAS.Initializer.holesPairingEquiv line 330
  34. lemma OAI.MatchingFPRAS.Initializer.matchings_card line 352
  35. lemma OAI.MatchingFPRAS.Initializer.uniform_weight line 364
  36. theorem OAI.MatchingFPRAS.Initializer.uniform_partition line 375
  37. lemma OAI.MatchingFPRAS.Initializer.pairingCount_pos_of_even line 382
  38. lemma OAI.MatchingFPRAS.Initializer.uniform_hole_ratio line 390
  39. def OAI.MatchingFPRAS.Initializer.initialScale line 408
  40. lemma OAI.MatchingFPRAS.Initializer.sqrt_square_bounds line 410
  41. lemma OAI.MatchingFPRAS.Initializer.initialScale_pos line 427
  42. theorem OAI.MatchingFPRAS.Initializer.initial_balanced line 432