OAI/Combinatorics/MatchingCount/Sampling/TreeIndexedPair.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.ExecutablePair.Context line 9
  2. def OAI.MatchingFPRAS.ExecutablePair.endpoints line 10
  3. def OAI.MatchingFPRAS.ExecutablePair.endpointsRealizer line 11
  4. lemma OAI.MatchingFPRAS.ExecutablePair.polynomial_endpoints line 12
  5. def OAI.MatchingFPRAS.ExecutablePair.incident line 16
  6. def OAI.MatchingFPRAS.ExecutablePair.incidentRealizer line 17
  7. lemma OAI.MatchingFPRAS.ExecutablePair.polynomial_incident line 20
  8. def OAI.MatchingFPRAS.ExecutablePair.same line 25
  9. def OAI.MatchingFPRAS.ExecutablePair.sameRealizer line 27
  10. lemma OAI.MatchingFPRAS.ExecutablePair.polynomial_same line 33
  11. def OAI.MatchingFPRAS.ExecutablePair.adjacent line 38
  12. def OAI.MatchingFPRAS.ExecutablePair.adjacentRealizer line 40
  13. lemma OAI.MatchingFPRAS.ExecutablePair.polynomial_adjacent line 43
  14. def OAI.MatchingFPRAS.ExecutablePair.p line 48
  15. def OAI.MatchingFPRAS.ExecutablePair.q line 49
  16. def OAI.MatchingFPRAS.ExecutablePair.r line 50
  17. def OAI.MatchingFPRAS.ExecutablePair.t line 51
  18. def OAI.MatchingFPRAS.ExecutablePair.u line 52
  19. def OAI.MatchingFPRAS.ExecutablePair.v line 53
  20. def OAI.MatchingFPRAS.ExecutablePair.pRealizer line 54
  21. def OAI.MatchingFPRAS.ExecutablePair.qRealizer line 55
  22. def OAI.MatchingFPRAS.ExecutablePair.rRealizer line 57
  23. def OAI.MatchingFPRAS.ExecutablePair.tRealizer line 58
  24. def OAI.MatchingFPRAS.ExecutablePair.uRealizer line 60
  25. def OAI.MatchingFPRAS.ExecutablePair.vRealizer line 61
  26. lemma OAI.MatchingFPRAS.ExecutablePair.polynomial_p line 62
  27. lemma OAI.MatchingFPRAS.ExecutablePair.polynomial_q line 67
  28. lemma OAI.MatchingFPRAS.ExecutablePair.polynomial_r line 72
  29. lemma OAI.MatchingFPRAS.ExecutablePair.polynomial_t line 77
  30. lemma OAI.MatchingFPRAS.ExecutablePair.polynomial_u line 82
  31. lemma OAI.MatchingFPRAS.ExecutablePair.polynomial_v line 86
  32. def OAI.MatchingFPRAS.ExecutablePair.draw line 91
  33. def OAI.MatchingFPRAS.ExecutablePair.drawRealizer line 92
  34. lemma OAI.MatchingFPRAS.ExecutablePair.polynomial_draw line 94