OAI/NumberTheory/PrimeGaps/EulerFactors.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.norm_prod_linear_remainder line 19
  2. theorem OAI.LargePrimeGaps.norm_one_sub_lower line 46
  3. theorem OAI.LargePrimeGaps.norm_one_sub_zpow_le line 52
  4. theorem OAI.LargePrimeGaps.norm_one_sub_zpow_sub_one line 72
  5. theorem OAI.LargePrimeGaps.norm_one_sub_zpow_linear line 86
  6. def OAI.LargePrimeGaps.genericLocalQuotient line 100
  7. theorem OAI.LargePrimeGaps.genericLocalQuotient_error line 104
  8. theorem OAI.LargePrimeGaps.norm_exp_sub_one_le_of_re_nonpos line 157
  9. def OAI.LargePrimeGaps.primeMonomial line 174
  10. theorem OAI.LargePrimeGaps.primeMonomial_norm_le line 177
  11. theorem OAI.LargePrimeGaps.primeMonomial_sub_one line 187
  12. theorem OAI.LargePrimeGaps.primeMonomial_zero line 201
  13. def OAI.LargePrimeGaps.eulerP line 204
  14. def OAI.LargePrimeGaps.eulerH line 207
  15. theorem OAI.LargePrimeGaps.sign_zpow_cases line 210
  16. theorem OAI.LargePrimeGaps.primeMonomial_scaled_norm line 215
  17. theorem OAI.LargePrimeGaps.delta_bounds line 221
  18. theorem OAI.LargePrimeGaps.eulerH_generic_eq line 241
  19. theorem OAI.LargePrimeGaps.eulerH_generic_error line 257
  20. theorem OAI.LargePrimeGaps.norm_one_sub_zpow_sub line 274
  21. theorem OAI.LargePrimeGaps.prime_inv_le_half line 293
  22. theorem OAI.LargePrimeGaps.norm_eulerP_le line 299
  23. theorem OAI.LargePrimeGaps.norm_eulerT_le line 322
  24. theorem OAI.LargePrimeGaps.norm_eulerH_le line 343
  25. theorem OAI.LargePrimeGaps.norm_eulerP_sub_zero_le line 353
  26. theorem OAI.LargePrimeGaps.norm_eulerT_sub_zero_le line 385
  27. theorem OAI.LargePrimeGaps.norm_eulerH_sub_zero_le line 432