OAI/Combinatorics/MatchingCount/Sampling/TreePrepareLadder.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.NumericLadder.Prepared line 10
  2. def OAI.MatchingFPRAS.NumericLadder.prepareContext line 12
  3. def OAI.MatchingFPRAS.NumericLadder.prepareContextRealizer line 14
  4. lemma OAI.MatchingFPRAS.NumericLadder.polynomial_prepareContext line 17
  5. def OAI.MatchingFPRAS.NumericLadder.baseTest line 25
  6. def OAI.MatchingFPRAS.NumericLadder.baseTestRealizer line 26
  7. lemma OAI.MatchingFPRAS.NumericLadder.polynomial_baseTest line 29
  8. def OAI.MatchingFPRAS.NumericLadder.baseSet line 36
  9. def OAI.MatchingFPRAS.NumericLadder.baseSetRealizer line 37
  10. lemma OAI.MatchingFPRAS.NumericLadder.polynomial_baseSet line 39
  11. lemma OAI.MatchingFPRAS.NumericLadder.baseSet_source line 43
  12. def OAI.MatchingFPRAS.NumericLadder.prepareSetup line 57
  13. def OAI.MatchingFPRAS.NumericLadder.prepareSetupRealizer line 59
  14. lemma OAI.MatchingFPRAS.NumericLadder.polynomial_prepareSetup line 63
  15. def OAI.MatchingFPRAS.NumericLadder.prepareState line 73
  16. def OAI.MatchingFPRAS.NumericLadder.prepareStateRealizer line 75
  17. lemma OAI.MatchingFPRAS.NumericLadder.polynomial_prepareState line 77
  18. abbrev OAI.MatchingFPRAS.NumericLadder.PreparedInput line 85
  19. def OAI.MatchingFPRAS.NumericLadder.preparedRun line 86
  20. def OAI.MatchingFPRAS.NumericLadder.preparedRunRealizer line 87
  21. lemma OAI.MatchingFPRAS.NumericLadder.polynomial_preparedRun line 88
  22. def OAI.MatchingFPRAS.NumericLadder.preparedTop line 93
  23. def OAI.MatchingFPRAS.NumericLadder.preparedTopRealizer line 94
  24. lemma OAI.MatchingFPRAS.NumericLadder.polynomial_preparedTop line 96
  25. theorem OAI.MatchingFPRAS.NumericLadder.preparedTop_post line 103