OAI/NumberTheory/SingleFold/QuadraticHeight.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingleFold.QuadraticLimit.sequence line 13
  2. lemma OAI.SingleFold.QuadraticLimit.step_bound line 21
  3. lemma OAI.SingleFold.QuadraticLimit.sequence_cauchy line 40
  4. def OAI.SingleFold.QuadraticLimit.limit line 43
  5. lemma OAI.SingleFold.QuadraticLimit.tendsto_sequence line 46
  6. lemma OAI.SingleFold.QuadraticLimit.error_bound line 50
  7. lemma OAI.SingleFold.QuadraticLimit.limit_zero line 57
  8. lemma OAI.SingleFold.QuadraticLimit.limit_nonneg line 64
  9. lemma OAI.SingleFold.QuadraticLimit.limit_parallelogram line 69
  10. lemma OAI.SingleFold.QuadraticLimit.limit_nsmul line 96
  11. lemma OAI.SingleFold.QuadraticLimit.limit_neg line 109
  12. lemma OAI.SingleFold.QuadraticLimit.limit_zsmul line 115
  13. lemma OAI.SingleFold.CurveHeight.naiveHeight_zero line 132
  14. lemma OAI.SingleFold.CurveHeight.naiveHeight_nonneg line 136
  15. lemma OAI.SingleFold.CurveHeight.naiveHeight_some line 138
  16. lemma OAI.SingleFold.CurveHeight.finite_x_fiber line 142
  17. instance OAI.SingleFold.CurveHeight.(instance at line 152) line 152
  18. def OAI.SingleFold.CurveHeight.canonicalHeight line 167
  19. lemma OAI.SingleFold.CurveHeight.canonicalHeight_limit line 170
  20. lemma OAI.SingleFold.CurveHeight.canonicalHeight_nonneg line 177
  21. lemma OAI.SingleFold.CurveHeight.canonicalHeight_zero line 182
  22. lemma OAI.SingleFold.CurveHeight.canonicalHeight_zsmul line 186
  23. lemma OAI.SingleFold.CurveHeight.canonicalHeight_nsmul line 193
  24. theorem OAI.SingleFold.CurveHeight.uniform_height line 197
  25. theorem OAI.SingleFold.CurveHeight.canonicalHeight_pos line 209