OAI/Combinatorics/MatchingCount/Complexity/TreePolynomialArithmetic.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatchingFPRAS.TreeTyped.weight_bool line 10
2. lemma OAI.MatchingFPRAS.TreeTyped.weight_bits line 11
3. lemma OAI.MatchingFPRAS.TreeTyped.weight_nat line 12
4. lemma OAI.MatchingFPRAS.TreeTyped.weight_nat_le line 13
5. lemma OAI.MatchingFPRAS.TreeTyped.size_le_weight line 15
6. lemma OAI.MatchingFPRAS.TreeTyped.weight_nat_small line 17
7. lemma OAI.MatchingFPRAS.TreeTyped.nat_size_add line 22
8. lemma OAI.MatchingFPRAS.TreeTyped.nat_size_mul line 27
9. lemma OAI.MatchingFPRAS.TreeTyped.weight_add line 32
10. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_add line 39
11. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_less line 48
12. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_subtract line 57
13. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_toBits line 70
14. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_listCons line 75
15. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_double line 80