OAI/Combinatorics/MatchingCount/Sampling/TreeCategorical.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.TreeFraction.sum line 11
  2. def OAI.MatchingFPRAS.TreeFraction.sumRealizer line 12
  3. lemma OAI.MatchingFPRAS.TreeFraction.fold_den line 15
  4. lemma OAI.MatchingFPRAS.TreeFraction.fold_val line 20
  5. lemma OAI.MatchingFPRAS.TreeFraction.sum_den line 31
  6. lemma OAI.MatchingFPRAS.TreeFraction.sum_val line 32
  7. def OAI.MatchingFPRAS.TreeFraction.cumulativeFraction line 37
  8. def OAI.MatchingFPRAS.TreeFraction.cumulativeFractionRealizer line 38
  9. lemma OAI.MatchingFPRAS.TreeFraction.cumulativeFraction_val line 39
  10. def OAI.MatchingFPRAS.TreeTyped.bitValue line 53
  11. def OAI.MatchingFPRAS.TreeTyped.bitDenominator line 61
  12. lemma OAI.MatchingFPRAS.TreeTyped.bitDenominator_eq line 62
  13. def OAI.MatchingFPRAS.TreeTyped.bitDenominatorRealizer line 69
  14. def OAI.MatchingFPRAS.ExecutableChoice.predicate line 77
  15. def OAI.MatchingFPRAS.ExecutableChoice.predicateRealizer line 79
  16. def OAI.MatchingFPRAS.ExecutableChoice.choose line 84
  17. def OAI.MatchingFPRAS.ExecutableChoice.chooseRealizer line 87
  18. lemma OAI.MatchingFPRAS.ExecutableChoice.choose_eq line 93
  19. def OAI.MatchingFPRAS.ExecutableChoice.chooseBits line 112
  20. def OAI.MatchingFPRAS.ExecutableChoice.chooseBitsRealizer line 114
  21. lemma OAI.MatchingFPRAS.ExecutableChoice.chooseBits_eq line 118