OAI/Computability/RationalHitting/BinomialBounds.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalHitting.StackLanguage.Binomial.allFactors line 8
  2. def OAI.RationalHitting.StackLanguage.Binomial.factored line 10
  3. lemma OAI.RationalHitting.StackLanguage.Binomial.eval_allFactors line 13
  4. def OAI.RationalHitting.StackLanguage.Binomial.cleanMul line 33
  5. lemma OAI.RationalHitting.StackLanguage.Binomial.eval_cleanMul line 34
  6. lemma OAI.RationalHitting.StackLanguage.Binomial.eval_cleanQuotient line 45
  7. lemma OAI.RationalHitting.StackLanguage.Binomial.eval_copy_clean line 60
  8. def OAI.RationalHitting.StackLanguage.Binomial.ratio line 69
  9. def OAI.RationalHitting.StackLanguage.Binomial.width line 74
  10. def OAI.RationalHitting.StackLanguage.Binomial.ratioCost line 75
  11. lemma OAI.RationalHitting.StackLanguage.Binomial.eval_ratio line 78
  12. def OAI.RationalHitting.StackLanguage.Binomial.compute line 153
  13. def OAI.RationalHitting.StackLanguage.Binomial.discard line 154
  14. def OAI.RationalHitting.StackLanguage.Binomial.choose line 155
  15. def OAI.RationalHitting.StackLanguage.Binomial.cost line 156
  16. theorem OAI.RationalHitting.StackLanguage.Binomial.eval_choose line 161

    Source documentation

    A single finite program for every binomial coefficient; the inputs are unary counters, not a factorial oracle. The out-of-range case is tested by the actual stack guard.

    theorem eval_choose (n k : ℕ) : ∃ t≤cost n k,
    Eval choose (input n k) (update (input n k) 0 (n.choose k).bits) t := by
…

    Mentions: OAI.RationalHitting.StackLanguage.Binomial.cost, OAI.RationalHitting.StackLanguage.Eval, OAI.RationalHitting.StackLanguage.Binomial.choose, OAI.RationalHitting.StackLanguage.Binomial.input

  17. lemma OAI.RationalHitting.StackLanguage.Binomial.factorCost_bound line 191
  18. lemma OAI.RationalHitting.StackLanguage.Binomial.width_bound line 207
  19. lemma OAI.RationalHitting.StackLanguage.Binomial.cost_bound line 216
  20. theorem OAI.RationalHitting.StackLanguage.Binomial.eval_choose_polynomial line 247

    Source documentation

    The exact binary binomial coefficient with a fixed polynomial bound in the unary input length.

    theorem eval_choose_polynomial (n k : ℕ) : ∃ t≤3000000*(n+k+1)^10,
    Eval choose (input n k) (update (input n k) 0 (n.choose k).bits) t := by
…

    Mentions: OAI.RationalHitting.StackLanguage.Eval, OAI.RationalHitting.StackLanguage.Binomial.choose, OAI.RationalHitting.StackLanguage.Binomial.input