OAI/Combinatorics/MatchingCount/Sampling/TreeScanChoice.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.ExecutableLadder.ScanSetup line 15
  2. def OAI.MatchingFPRAS.ExecutableLadder.updateList line 17
  3. def OAI.MatchingFPRAS.ExecutableLadder.updateListRealizer line 21
  4. lemma OAI.MatchingFPRAS.ExecutableLadder.polynomial_updateList line 27
  5. def OAI.MatchingFPRAS.ExecutableLadder.updateEqual line 38
  6. lemma OAI.MatchingFPRAS.ExecutableLadder.polynomial_updateEqual line 43
  7. def OAI.MatchingFPRAS.ExecutableLadder.updateSetRealizer line 47
  8. lemma OAI.MatchingFPRAS.ExecutableLadder.polynomial_updateSet line 53
  9. def OAI.MatchingFPRAS.ExecutableLadder.scanChoice line 64
  10. def OAI.MatchingFPRAS.ExecutableLadder.scanChoiceRealizer line 67
  11. lemma OAI.MatchingFPRAS.ExecutableLadder.polynomial_scanChoice line 73
  12. lemma OAI.MatchingFPRAS.ExecutableLadder.updateSet_eq line 92
  13. lemma OAI.MatchingFPRAS.ExecutableLadder.scanChoice_eq line 99