OAI/Combinatorics/MatchingCount/Sampling/TreeFastSample.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MatchingFPRAS.ExecutableUnit.fastRawSampleline 12 - def
OAI.MatchingFPRAS.ExecutableUnit.unwindClippedline 18 - lemma
OAI.MatchingFPRAS.ExecutableUnit.fastDescend_unwindline 20 - def
OAI.MatchingFPRAS.ExecutableUnit.fastSampleline 38 - def
OAI.MatchingFPRAS.ExecutableUnit.fastSampleRealizerline 39 - lemma
OAI.MatchingFPRAS.ExecutableUnit.polynomial_fastSampleline 44 - lemma
OAI.MatchingFPRAS.ExecutableUnit.fastSelected_eq_of_getDline 52 - lemma
OAI.MatchingFPRAS.ExecutableUnit.fastRawSample_eqline 69 - lemma
OAI.MatchingFPRAS.ExecutableUnit.fastSample_eqline 120