OAI/Combinatorics/MatchingCount/Sampling/TreeScanRun.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.MatchingFPRAS.ExecutableLadder.RunSetupline 14 - abbrev
OAI.MatchingFPRAS.ExecutableLadder.RunStateline 15 - def
OAI.MatchingFPRAS.ExecutableLadder.runStepline 17 - def
OAI.MatchingFPRAS.ExecutableLadder.runStepRealizerline 20 - lemma
OAI.MatchingFPRAS.ExecutableLadder.polynomial_runStepline 28 - lemma
OAI.MatchingFPRAS.ExecutableLadder.fold_runStepline 43 - lemma
OAI.MatchingFPRAS.ExecutableLadder.fold_normalized_weightline 53 - lemma
OAI.MatchingFPRAS.ExecutableLadder.polynomial_scanRunline 63 - lemma
OAI.MatchingFPRAS.ExecutableLadder.scanRun_repline 96