OAI/Combinatorics/MatchingCount/Machines/TreeSlotWeight.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.TreeFraction.add_repr line 11
  2. lemma OAI.MatchingFPRAS.TreeFraction.repr_nat line 18
  3. def OAI.MatchingFPRAS.TreeFraction.fuelPower line 20
  4. def OAI.MatchingFPRAS.TreeFraction.fuelPowerRealizer line 21
  5. lemma OAI.MatchingFPRAS.TreeFraction.polynomial_fuelPower line 22
  6. lemma OAI.MatchingFPRAS.TreeFraction.fuelPower_repr line 24
  7. def OAI.MatchingFPRAS.ExecutableLadder.tierBase line 36
  8. def OAI.MatchingFPRAS.ExecutableLadder.tierBaseRealizer line 37
  9. lemma OAI.MatchingFPRAS.ExecutableLadder.polynomial_tierBase line 39
  10. lemma OAI.MatchingFPRAS.ExecutableLadder.tierBase_repr line 45
  11. abbrev OAI.MatchingFPRAS.ExecutableLadder.TierInput line 52
  12. def OAI.MatchingFPRAS.ExecutableLadder.tierPower line 54
  13. def OAI.MatchingFPRAS.ExecutableLadder.tierPowerRealizer line 56
  14. lemma OAI.MatchingFPRAS.ExecutableLadder.polynomial_tierPower line 58
  15. lemma OAI.MatchingFPRAS.ExecutableLadder.tierPower_repr line 65
  16. def OAI.MatchingFPRAS.ExecutableLadder.slotWeight line 70
  17. def OAI.MatchingFPRAS.ExecutableLadder.slotWeightRealizer line 72
  18. lemma OAI.MatchingFPRAS.ExecutableLadder.polynomial_slotWeight line 76
  19. lemma OAI.MatchingFPRAS.ExecutableLadder.slotWeight_repr line 85
  20. lemma OAI.MatchingFPRAS.ExecutableLadder.slotWeight_source line 96