OAI/Combinatorics/MatchingCount/Sampling/TreePreparedMarked.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.NumericMarking.SampleContext line 10
  2. abbrev OAI.MatchingFPRAS.NumericMarking.SampleBits line 11
  3. abbrev OAI.MatchingFPRAS.NumericMarking.SampleInput line 12
  4. def OAI.MatchingFPRAS.NumericMarking.sample line 14
  5. def OAI.MatchingFPRAS.NumericMarking.sampleRealizer line 16
  6. lemma OAI.MatchingFPRAS.NumericMarking.polynomial_sample line 18
  7. def OAI.MatchingFPRAS.NumericMarking.sampleMany line 25
  8. def OAI.MatchingFPRAS.NumericMarking.sampleManyRealizer line 27
  9. lemma OAI.MatchingFPRAS.NumericMarking.polynomial_sampleMany line 28
  10. theorem OAI.MatchingFPRAS.NumericMarking.sampleMany_post line 30
  11. lemma OAI.MatchingFPRAS.NumericMarking.sample_source line 47