OAI/Combinatorics/MatchingCount/Algorithm/TreeEstimator.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.TreeFraction.fold_sum_repr line 7
  2. lemma OAI.MatchingFPRAS.TreeFraction.sum_repr line 18
  3. def OAI.MatchingFPRAS.ExecutableEstimator.mean line 27
  4. def OAI.MatchingFPRAS.ExecutableEstimator.meanRealizer line 28
  5. lemma OAI.MatchingFPRAS.ExecutableEstimator.polynomial_mean line 30
  6. lemma OAI.MatchingFPRAS.ExecutableEstimator.mean_rep line 34
  7. def OAI.MatchingFPRAS.ExecutableEstimator.ratio line 39
  8. def OAI.MatchingFPRAS.ExecutableEstimator.ratioRealizer line 41
  9. lemma OAI.MatchingFPRAS.ExecutableEstimator.polynomial_ratio line 44
  10. lemma OAI.MatchingFPRAS.ExecutableEstimator.ratio_rep line 50
  11. def OAI.MatchingFPRAS.ExecutableEstimator.upper line 60
  12. def OAI.MatchingFPRAS.ExecutableEstimator.upperRealizer line 64
  13. lemma OAI.MatchingFPRAS.ExecutableEstimator.polynomial_upper line 72
  14. lemma OAI.MatchingFPRAS.ExecutableEstimator.upper_rep line 83