OAI/NumberTheory/SingleFold/EllipticGrowth.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SingleFold.EllipticModel.E line 7
  2. def OAI.SingleFold.EllipticModel.Hx line 9
  3. lemma OAI.SingleFold.EllipticModel.Hx_pos line 12
  4. lemma OAI.SingleFold.EllipticModel.log_Hx line 16
  5. lemma OAI.SingleFold.EllipticModel.Hx_neg line 20
  6. def OAI.SingleFold.EllipticModel.point line 27
  7. def OAI.SingleFold.EllipticModel.P line 28
  8. def OAI.SingleFold.EllipticModel.index line 29
  9. lemma OAI.SingleFold.EllipticModel.point_add line 30
  10. lemma OAI.SingleFold.EllipticModel.point_zero line 34
  11. lemma OAI.SingleFold.EllipticModel.point_int line 38
  12. lemma OAI.SingleFold.EllipticModel.point_split line 42
  13. lemma OAI.SingleFold.EllipticModel.point_nsmul line 44
  14. lemma OAI.SingleFold.EllipticModel.point_torsion line 48
  15. lemma OAI.SingleFold.EllipticModel.double_torsion line 53
  16. lemma OAI.SingleFold.EllipticModel.P_nontorsion line 55
  17. lemma OAI.SingleFold.EllipticModel.normal_form line 61
  18. def OAI.SingleFold.EllipticModel.W line 69
  19. def OAI.SingleFold.EllipticModel.sequence line 70
  20. lemma OAI.SingleFold.EllipticModel.W_pos line 71
  21. lemma OAI.SingleFold.EllipticModel.sequence_zero line 72
  22. lemma OAI.SingleFold.EllipticModel.W_neg line 76
  23. lemma OAI.SingleFold.EllipticModel.W_point line 79
  24. lemma OAI.SingleFold.EllipticModel.W_index line 85
  25. lemma OAI.SingleFold.EllipticModel.sequence_approx line 97
  26. def OAI.SingleFold.EllipticModel.xcoord line 106
  27. def OAI.SingleFold.EllipticModel.ycoord line 109
  28. lemma OAI.SingleFold.EllipticModel.xcoord_neg line 112
  29. lemma OAI.SingleFold.EllipticModel.ycoord_neg line 113
  30. lemma OAI.SingleFold.EllipticModel.xy_unique line 117
  31. lemma OAI.SingleFold.EllipticModel.index_point line 135
  32. lemma OAI.SingleFold.EllipticModel.index_zero line 136
  33. lemma OAI.SingleFold.EllipticModel.index_add line 137
  34. lemma OAI.SingleFold.EllipticModel.index_neg line 138
  35. lemma OAI.SingleFold.EllipticModel.point_ne_zero line 139
  36. def OAI.SingleFold.EllipticModel.Representative line 145
  37. lemma OAI.SingleFold.EllipticModel.representative_max line 148
  38. lemma OAI.SingleFold.EllipticModel.representative_unique line 178
  39. lemma OAI.SingleFold.EllipticModel.representative_exists line 183
  40. theorem OAI.SingleFold.EllipticModel.height_constants line 217
  41. lemma OAI.SingleFold.EllipticModel.neighbor_index line 249
  42. lemma OAI.SingleFold.EllipticModel.index_P line 258
  43. lemma OAI.SingleFold.EllipticModel.neighbor_max line 259
  44. lemma OAI.SingleFold.EllipticModel.double_index line 268
  45. lemma OAI.SingleFold.EllipticModel.representative_index_pos line 272
  46. def OAI.SingleFold.EllipticModel.Bracket line 281
  47. def OAI.SingleFold.EllipticModel.Window line 283
  48. lemma OAI.SingleFold.EllipticModel.sequence_one line 286
  49. lemma OAI.SingleFold.EllipticModel.bracket_iff line 287
  50. lemma OAI.SingleFold.EllipticModel.window_iff line 293
  51. def OAI.SingleFold.EllipticModel.GrowthPair line 304
  52. lemma OAI.SingleFold.EllipticModel.growth_pair_existsUnique line 307
  53. theorem OAI.SingleFold.EllipticModel.growth_model line 327
  54. abbrev OAI.SingleFold.GrowthCompilation.E line 370
  55. lemma OAI.SingleFold.GrowthCompilation.encoded_height line 371
  56. lemma OAI.SingleFold.GrowthCompilation.encoded_x line 376
  57. lemma OAI.SingleFold.GrowthCompilation.encoded_y line 378
  58. lemma OAI.SingleFold.GrowthCompilation.height_sf line 380
  59. lemma OAI.SingleFold.GrowthCompilation.representative_sf line 389
  60. lemma OAI.SingleFold.GrowthCompilation.bracket_sf line 403
  61. lemma OAI.SingleFold.GrowthCompilation.window_sf line 415
  62. lemma OAI.SingleFold.GrowthCompilation.pair_sf line 426
  63. lemma OAI.SingleFold.GrowthCompilation.decode_injective_valid line 432
  64. lemma OAI.SingleFold.GrowthCompilation.graph_sf line 440
  65. theorem OAI.SingleFold.GrowthCompilation.growth line 487