OAI/Combinatorics/MatchingCount/Sampling/TreeNumericLadder.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.NumericLadder.PairSetup line 12
  2. abbrev OAI.MatchingFPRAS.NumericLadder.RefreshSetup line 13
  3. abbrev OAI.MatchingFPRAS.NumericLadder.Context line 14
  4. abbrev OAI.MatchingFPRAS.NumericLadder.Bits line 15
  5. def OAI.MatchingFPRAS.NumericLadder.row line 17
  6. def OAI.MatchingFPRAS.NumericLadder.rowRealizer line 18
  7. lemma OAI.MatchingFPRAS.NumericLadder.polynomial_row line 19
  8. def OAI.MatchingFPRAS.NumericLadder.guide line 24
  9. def OAI.MatchingFPRAS.NumericLadder.guideRealizer line 25
  10. lemma OAI.MatchingFPRAS.NumericLadder.polynomial_guide line 27
  11. def OAI.MatchingFPRAS.NumericLadder.pairContext line 33
  12. def OAI.MatchingFPRAS.NumericLadder.pairContextRealizer line 35
  13. lemma OAI.MatchingFPRAS.NumericLadder.polynomial_pairContext line 37
  14. def OAI.MatchingFPRAS.NumericLadder.pairDraw line 42
  15. def OAI.MatchingFPRAS.NumericLadder.pairRealizer line 44
  16. lemma OAI.MatchingFPRAS.NumericLadder.polynomial_pair line 47
  17. def OAI.MatchingFPRAS.NumericLadder.refresh line 54
  18. def OAI.MatchingFPRAS.NumericLadder.refreshRealizer line 56
  19. lemma OAI.MatchingFPRAS.NumericLadder.polynomial_refresh line 58
  20. abbrev OAI.MatchingFPRAS.NumericLadder.Input line 63
  21. def OAI.MatchingFPRAS.NumericLadder.execute line 64
  22. def OAI.MatchingFPRAS.NumericLadder.executeRealizer line 66
  23. lemma OAI.MatchingFPRAS.NumericLadder.polynomial_execute line 68
  24. theorem OAI.MatchingFPRAS.NumericLadder.execute_post line 72