OAI/Combinatorics/MatchingCount/Complexity/TreeCostMeasure.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatchingFPRAS.TreeTyped.WorkBound line 11
2. lemma OAI.MatchingFPRAS.TreeTyped.work_of_polynomial line 14
3. lemma OAI.MatchingFPRAS.TreeTyped.work_congr line 18
4. lemma OAI.MatchingFPRAS.TreeTyped.work_composition line 22
5. lemma OAI.MatchingFPRAS.TreeTyped.work_then_polynomial line 36
6. lemma OAI.MatchingFPRAS.TreeTyped.work_remeasure line 41
7. lemma OAI.MatchingFPRAS.TreeTyped.work_boundedRepeat line 47
8. lemma OAI.MatchingFPRAS.TreeTyped.weight_nat_numeric line 92
9. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_successor line 96
10. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_rangeStep line 98
11. lemma OAI.MatchingFPRAS.TreeTyped.range_numeric_work line 101
12. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_boundedRange line 129