OAI/Combinatorics/MatchingCount/Algorithm/TreeTierWeights.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.NumericLadder.TierData line 13
  2. def OAI.MatchingFPRAS.NumericLadder.slotCount line 15
  3. def OAI.MatchingFPRAS.NumericLadder.slotCountRealizer line 16
  4. lemma OAI.MatchingFPRAS.NumericLadder.polynomial_slotCount line 19
  5. lemma OAI.MatchingFPRAS.NumericLadder.slotCount_bound line 24
  6. def OAI.MatchingFPRAS.NumericLadder.slots line 29
  7. def OAI.MatchingFPRAS.NumericLadder.slotsRealizer line 30
  8. lemma OAI.MatchingFPRAS.NumericLadder.polynomial_slots line 31
  9. def OAI.MatchingFPRAS.NumericLadder.weightRow line 34
  10. def OAI.MatchingFPRAS.NumericLadder.weightRowRealizer line 36
  11. lemma OAI.MatchingFPRAS.NumericLadder.polynomial_weightRow line 39
  12. def OAI.MatchingFPRAS.NumericLadder.weightRows line 46
  13. def OAI.MatchingFPRAS.NumericLadder.weightRowsRealizer line 47
  14. lemma OAI.MatchingFPRAS.NumericLadder.polynomial_weightRows line 48
  15. lemma OAI.MatchingFPRAS.NumericLadder.index_enum line 53
  16. lemma OAI.MatchingFPRAS.NumericLadder.range_slot_indices line 55
  17. lemma OAI.MatchingFPRAS.NumericLadder.weightRows_source line 61
  18. theorem OAI.MatchingFPRAS.NumericLadder.weightRows_post line 82