OAI/Combinatorics/MatchingCount/Sampling/TreeLadderIndexed.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.NumericLadder.typedGuide line 14
  2. def OAI.MatchingFPRAS.NumericLadder.typedPair line 15
  3. def OAI.MatchingFPRAS.NumericLadder.typedRefresh line 17
  4. def OAI.MatchingFPRAS.NumericLadder.typedGuideRealizer line 18
  5. def OAI.MatchingFPRAS.NumericLadder.typedPairRealizer line 20
  6. def OAI.MatchingFPRAS.NumericLadder.typedRefreshRealizer line 22
  7. abbrev OAI.MatchingFPRAS.NumericLadder.TypedInput line 24
  8. def OAI.MatchingFPRAS.NumericLadder.typedExecute line 25
  9. def OAI.MatchingFPRAS.NumericLadder.typedExecuteRealizer line 27
  10. lemma OAI.MatchingFPRAS.NumericLadder.polynomial_typedExecute line 29
  11. lemma OAI.MatchingFPRAS.NumericLadder.inl_program_zero line 34
  12. lemma OAI.MatchingFPRAS.NumericLadder.inr_program_zero line 39
  13. lemma OAI.MatchingFPRAS.NumericLadder.lookup_program_zero line 47
  14. lemma OAI.MatchingFPRAS.NumericLadder.normalize_program_zero line 57
  15. lemma OAI.MatchingFPRAS.NumericLadder.none_encode_zero line 64
  16. lemma OAI.MatchingFPRAS.NumericLadder.choice_program_zero line 71
  17. lemma OAI.MatchingFPRAS.NumericLadder.local_program_zero line 81
  18. lemma OAI.MatchingFPRAS.NumericLadder.scan_program_zero line 88
  19. lemma OAI.MatchingFPRAS.NumericLadder.typedExecute_program line 95