OAI/NumberTheory/PrimeGaps/ZetaKernel.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.mangoldt_log_term_nonneg line 15
  2. theorem OAI.LargePrimeGaps.mangoldt_log_term_le line 19
  3. theorem OAI.LargePrimeGaps.prime_power_sum_le_log_zeta line 32
  4. theorem OAI.LargePrimeGaps.prime_reciprocal_rankin line 48
  5. theorem OAI.LargePrimeGaps.eventually_prime_reciprocal_bound line 74
  6. theorem OAI.LargePrimeGaps.zeta_pole_linear_error line 98
  7. theorem OAI.LargePrimeGaps.zeta_pole_two_sided line 112
  8. theorem OAI.LargePrimeGaps.norm_prod_sub_prod_le line 131
  9. theorem OAI.LargePrimeGaps.norm_prod_sub_one_le line 164
  10. def OAI.LargePrimeGaps.nonemptySubsets line 171
  11. theorem OAI.LargePrimeGaps.mem_nonemptySubsets line 175
  12. theorem OAI.LargePrimeGaps.sum_nonemptySubsets_sign line 180
  13. theorem OAI.LargePrimeGaps.prod_const_zpow line 187
  14. def OAI.LargePrimeGaps.fiberKernel line 194
  15. def OAI.LargePrimeGaps.fiberZeta line 197
  16. def OAI.LargePrimeGaps.normalizedFiberZeta line 200
  17. theorem OAI.LargePrimeGaps.fiberKernel_homogeneous line 203
  18. theorem OAI.LargePrimeGaps.fiberZeta_factorization line 212
  19. theorem OAI.LargePrimeGaps.norm_inv_sub_one_le line 225
  20. theorem OAI.LargePrimeGaps.normalizedFiberZeta_error line 232
  21. def OAI.LargePrimeGaps.frequencyW line 253
  22. theorem OAI.LargePrimeGaps.frequencyW_re line 255
  23. theorem OAI.LargePrimeGaps.frequencyW_norm line 257
  24. theorem OAI.LargePrimeGaps.frequencySum_re line 260
  25. theorem OAI.LargePrimeGaps.frequencySum_norm_lower line 263
  26. theorem OAI.LargePrimeGaps.frequencySum_ne_zero line 270
  27. theorem OAI.LargePrimeGaps.frequencySum_norm_upper line 274
  28. theorem OAI.LargePrimeGaps.fiberKernel_norm_polynomial line 282
  29. theorem OAI.LargePrimeGaps.fiberZeta_contour_error line 304