OAI/Combinatorics/MatchingCount/Arithmetic/TreeDyadic.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatchingFPRAS.ExecutableHierarchy.level line 10
2. def OAI.MatchingFPRAS.ExecutableHierarchy.levelRealizer line 11
3. lemma OAI.MatchingFPRAS.ExecutableHierarchy.polynomial_level line 13
4. lemma OAI.MatchingFPRAS.ExecutableHierarchy.findGreatest_lt_size line 17
5. lemma OAI.MatchingFPRAS.ExecutableHierarchy.level_val line 26
6. lemma OAI.MatchingFPRAS.ExecutableHierarchy.level_repr line 35
7. def OAI.MatchingFPRAS.ExecutableHierarchy.threshold line 39
8. def OAI.MatchingFPRAS.ExecutableHierarchy.thresholdRealizer line 40
9. lemma OAI.MatchingFPRAS.ExecutableHierarchy.polynomial_threshold line 41
10. lemma OAI.MatchingFPRAS.ExecutableHierarchy.threshold_repr line 44