OAI/NumberTheory/Ostmann/QuadraticSieveMainRemainder.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.QuadraticSieve.truncatedMainAlpha line 8
  2. def OAI.Ostmann.QuadraticSieve.truncatedMainBeta line 12
  3. def OAI.Ostmann.QuadraticSieve.mainRemainder line 17
  4. theorem OAI.Ostmann.QuadraticSieve.truncatedMainAlpha_eq_of_le line 20
  5. theorem OAI.Ostmann.QuadraticSieve.truncatedMainBeta_eq_of_le line 25
  6. theorem OAI.Ostmann.QuadraticSieve.mainRemainder_zero_of_le line 30
  7. theorem OAI.Ostmann.QuadraticSieve.truncatedMainAlpha_zero_of_lt line 35
  8. theorem OAI.Ostmann.QuadraticSieve.truncatedMainBeta_zero_of_lt line 49
  9. theorem OAI.Ostmann.QuadraticSieve.mainRemainder_support line 63
  10. theorem OAI.Ostmann.QuadraticSieve.abs_truncatedMainAlpha_le line 81
  11. theorem OAI.Ostmann.QuadraticSieve.abs_truncatedMainBeta_le line 96
  12. theorem OAI.Ostmann.QuadraticSieve.abs_mainRemainder_le line 111