OAI/Combinatorics/MatchingCount/Complexity/TreePolynomial.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.TreeTyped.weight line 11
  2. lemma OAI.MatchingFPRAS.TreeTyped.weight_prod line 12
  3. lemma OAI.MatchingFPRAS.TreeTyped.weight_nil line 13
  4. lemma OAI.MatchingFPRAS.TreeTyped.weight_cons line 14
  5. lemma OAI.MatchingFPRAS.TreeTyped.weight_pos line 15
  6. lemma OAI.MatchingFPRAS.TreeTyped.list_length_le_weight line 18
  7. lemma OAI.MatchingFPRAS.TreeTyped.weight_mem line 20
  8. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_eval_monotone line 22
  9. def OAI.MatchingFPRAS.TreeTyped.PolynomialBound line 27
  10. def OAI.MatchingFPRAS.TreeTyped.PolynomialTime line 29
  11. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_identity line 31
  12. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_first line 35
  13. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_second line 41
  14. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_composition line 48
  15. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_pair line 60
  16. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_congr line 71
  17. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_choose line 75
  18. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_constantData line 89
  19. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_constant line 95
  20. lemma OAI.MatchingFPRAS.TreeTyped.Fold.cost_prefix_bound line 99
  21. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_fold line 118