OAI/Combinatorics/MatchingCount/Sampling/TreeIndexedPairUniform.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.ExecutablePair.typedP line 11
  2. def OAI.MatchingFPRAS.ExecutablePair.typedQ line 12
  3. def OAI.MatchingFPRAS.ExecutablePair.typedR line 13
  4. def OAI.MatchingFPRAS.ExecutablePair.typedT line 14
  5. def OAI.MatchingFPRAS.ExecutablePair.typedU line 15
  6. def OAI.MatchingFPRAS.ExecutablePair.typedV line 16
  7. def OAI.MatchingFPRAS.ExecutablePair.typedPRealizer line 17
  8. def OAI.MatchingFPRAS.ExecutablePair.typedQRealizer line 19
  9. def OAI.MatchingFPRAS.ExecutablePair.typedRRealizer line 21
  10. def OAI.MatchingFPRAS.ExecutablePair.typedTRealizer line 23
  11. def OAI.MatchingFPRAS.ExecutablePair.typedURealizer line 25
  12. def OAI.MatchingFPRAS.ExecutablePair.typedVRealizer line 27
  13. lemma OAI.MatchingFPRAS.ExecutablePair.polynomial_typedP line 29
  14. lemma OAI.MatchingFPRAS.ExecutablePair.polynomial_typedQ line 31
  15. lemma OAI.MatchingFPRAS.ExecutablePair.polynomial_typedR line 33
  16. lemma OAI.MatchingFPRAS.ExecutablePair.polynomial_typedT line 35
  17. lemma OAI.MatchingFPRAS.ExecutablePair.polynomial_typedU line 37
  18. lemma OAI.MatchingFPRAS.ExecutablePair.polynomial_typedV line 39
  19. def OAI.MatchingFPRAS.ExecutablePair.typedDraw line 42
  20. def OAI.MatchingFPRAS.ExecutablePair.typedDrawRealizer line 43
  21. lemma OAI.MatchingFPRAS.ExecutablePair.polynomial_typedDraw line 46
  22. lemma OAI.MatchingFPRAS.ExecutablePair.typedDraw_program line 50
  23. lemma OAI.MatchingFPRAS.ExecutablePair.typedDraw_source line 58