OAI/Combinatorics/MatchingCount/Sampling/TreeScanRun.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.ExecutableLadder.RunSetup line 14
  2. abbrev OAI.MatchingFPRAS.ExecutableLadder.RunState line 15
  3. def OAI.MatchingFPRAS.ExecutableLadder.runStep line 17
  4. def OAI.MatchingFPRAS.ExecutableLadder.runStepRealizer line 20
  5. lemma OAI.MatchingFPRAS.ExecutableLadder.polynomial_runStep line 28
  6. lemma OAI.MatchingFPRAS.ExecutableLadder.fold_runStep line 43
  7. lemma OAI.MatchingFPRAS.ExecutableLadder.fold_normalized_weight line 53
  8. lemma OAI.MatchingFPRAS.ExecutableLadder.polynomial_scanRun line 63
  9. lemma OAI.MatchingFPRAS.ExecutableLadder.scanRun_rep line 96