OAI/NumberTheory/SingleFold/Pell.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleFold.PellPower.y_positive line 9
  2. lemma OAI.SingleFold.PellPower.step_bounds line 12
  3. lemma OAI.SingleFold.PellPower.power_bounds line 20
  4. def OAI.SingleFold.PellPower.rate line 36
  5. lemma OAI.SingleFold.PellPower.rate_bounds line 38
  6. lemma OAI.SingleFold.PellPower.rate_pos line 49
  7. lemma OAI.SingleFold.PellPower.rate_zero line 54
  8. lemma OAI.SingleFold.PellPower.rate_succ line 59
  9. lemma OAI.SingleFold.PellPower.ratio_rate line 72
  10. lemma OAI.SingleFold.PellPower.ratio_bounds line 88
  11. lemma OAI.SingleFold.PellAnalytics.reciprocal_binomial line 125
  12. lemma OAI.SingleFold.PellAnalytics.binomial_error line 134
  13. lemma OAI.SingleFold.PellAnalytics.index_cutoff_real line 139
  14. lemma OAI.SingleFold.PellAnalytics.index_cutoff line 160
  15. lemma OAI.SingleFold.PellAnalytics.quotient_error line 173
  16. lemma OAI.SingleFold.PellSystem.index_pinned line 204
  17. lemma OAI.SingleFold.PellSystem.pell_pinned line 231
  18. lemma OAI.SingleFold.PellSystem.quotient_sound line 243
  19. lemma OAI.SingleFold.PellSystem.residue_exists line 273