OAI/NumberTheory/SingleFold/Power.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleFold.PowerEstimate.choose_ell line 6
  2. def OAI.SingleFold.PowerEstimate.input line 16
  3. lemma OAI.SingleFold.PowerEstimate.input_bounds line 17
  4. lemma OAI.SingleFold.PowerEstimate.growth_nat line 34
  5. lemma OAI.SingleFold.PowerEstimate.cutoff line 50
  6. def OAI.SingleFold.PowerSystem.System line 101
  7. lemma OAI.SingleFold.PowerSystem.pell_eq line 108
  8. def OAI.SingleFold.PowerSystem.px line 113
  9. def OAI.SingleFold.PowerSystem.py line 114
  10. lemma OAI.SingleFold.PowerSystem.coords_eq line 115
  11. lemma OAI.SingleFold.PowerSystem.pinned line 126
  12. lemma OAI.SingleFold.PowerSystem.sound line 140
  13. lemma OAI.SingleFold.PowerSystem.unique line 151
  14. lemma OAI.SingleFold.PowerSystem.complete line 174
  15. lemma OAI.SingleFold.Compiler.ScalarSF.reindex line 228
  16. lemma OAI.SingleFold.Compiler.ScalarSF.sub line 230
  17. lemma OAI.SingleFold.PowerCompilation.system_sf line 249
  18. lemma OAI.SingleFold.PowerCompilation.power_of_growth line 279
  19. theorem OAI.SingleFold.PowerCompilation.power line 299