OAI/NumberTheory/PrimeGaps/FourierNormalization.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargePrimeGaps.frequencyDilation line 28
  2. theorem OAI.LargePrimeGaps.frequencyDilation_apply line 32
  3. def OAI.LargePrimeGaps.radianFourier line 35
  4. theorem OAI.LargePrimeGaps.radianFourier_apply line 39
  5. theorem OAI.LargePrimeGaps.radianFourier_inversion line 54
  6. def OAI.LargePrimeGaps.laplaceSchwartz line 88
  7. theorem OAI.LargePrimeGaps.laplaceSchwartz_apply line 94
  8. def OAI.LargePrimeGaps.sourceFourier line 98
  9. theorem OAI.LargePrimeGaps.sourceFourier_apply line 102
  10. theorem OAI.LargePrimeGaps.sourceFourier_inversion line 113
  11. theorem OAI.LargePrimeGaps.sourceFourier_integrable_pow_mul line 130
  12. def OAI.LargePrimeGaps.primePrefix line 137
  13. theorem OAI.LargePrimeGaps.mem_primePrefix line 139
  14. def OAI.LargePrimeGaps.eulerGlobal line 144
  15. def OAI.LargePrimeGaps.genericEulerConstant line 148
  16. theorem OAI.LargePrimeGaps.genericEulerConstant_nonneg line 151
  17. theorem OAI.LargePrimeGaps.eulerH_summable_error line 155
  18. theorem OAI.LargePrimeGaps.eulerH_tail_sum line 174
  19. def OAI.LargePrimeGaps.primeReciprocalPrefix line 193
  20. theorem OAI.LargePrimeGaps.eulerGlobal_comparison line 196
  21. theorem OAI.LargePrimeGaps.eq_of_emod_eq_of_bound line 263
  22. theorem OAI.LargePrimeGaps.residueFamily_generic_of_bound line 273
  23. theorem OAI.LargePrimeGaps.markedResidueFamily_generic_of_bound line 278
  24. theorem OAI.LargePrimeGaps.subsetFamily_card_le line 286
  25. theorem OAI.LargePrimeGaps.unmarked_eulerGlobal_comparison line 291
  26. theorem OAI.LargePrimeGaps.marked_eulerGlobal_comparison line 304
  27. theorem OAI.LargePrimeGaps.singularSeries_cast_hasProd line 317
  28. theorem OAI.LargePrimeGaps.unmarked_eulerGlobal_zero line 322
  29. theorem OAI.LargePrimeGaps.marked_eulerGlobal_zero line 329
  30. theorem OAI.LargePrimeGaps.primeMonomial_cpow line 337
  31. def OAI.LargePrimeGaps.eulerZetaProduct line 347
  32. theorem OAI.LargePrimeGaps.eulerZetaProduct_hasProd line 350
  33. theorem OAI.LargePrimeGaps.eulerZetaProduct_ne_zero line 368
  34. theorem OAI.LargePrimeGaps.local_zeta_factor_ne_zero line 378
  35. theorem OAI.LargePrimeGaps.eulerP_eq_eulerH_mul line 388
  36. theorem OAI.LargePrimeGaps.eulerP_hasProd line 401
  37. abbrev OAI.LargePrimeGaps.EulerChoices line 409
  38. def OAI.LargePrimeGaps.eulerChoiceTerm line 412
  39. def OAI.LargePrimeGaps.eulerChoiceNorm line 416
  40. theorem OAI.LargePrimeGaps.eulerChoiceNorm_nonneg line 419
  41. theorem OAI.LargePrimeGaps.eulerChoice_sum_norm line 423
  42. theorem OAI.LargePrimeGaps.eulerChoice_sum line 431
  43. theorem OAI.LargePrimeGaps.eulerChoice_summable_norm line 439
  44. theorem OAI.LargePrimeGaps.eulerChoices_hasProd line 448