OAI/Combinatorics/MatchingCount/Sampling/TreePreparedMarked.lean
11 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.MatchingFPRAS.NumericMarking.SampleContextline 10 - abbrev
OAI.MatchingFPRAS.NumericMarking.SampleBitsline 11 - abbrev
OAI.MatchingFPRAS.NumericMarking.SampleInputline 12 - def
OAI.MatchingFPRAS.NumericMarking.sampleline 14 - def
OAI.MatchingFPRAS.NumericMarking.sampleRealizerline 16 - lemma
OAI.MatchingFPRAS.NumericMarking.polynomial_sampleline 18 - def
OAI.MatchingFPRAS.NumericMarking.sampleManyline 25 - def
OAI.MatchingFPRAS.NumericMarking.sampleManyRealizerline 27 - lemma
OAI.MatchingFPRAS.NumericMarking.polynomial_sampleManyline 28 - theorem
OAI.MatchingFPRAS.NumericMarking.sampleMany_postline 30 - lemma
OAI.MatchingFPRAS.NumericMarking.sample_sourceline 47