OAI/NumberTheory/DirichletL/Hecke/MobiusEulerCorrection.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SmoothMobiusCorrection.PrimeIdeal line 86
  2. def OAI.SmoothMobiusCorrection.primeProduct line 88
  3. def OAI.SmoothMobiusCorrection.primeSet line 90
  4. theorem OAI.SmoothMobiusCorrection.mem_primeSet line 93
  5. theorem OAI.SmoothMobiusCorrection.primeProduct_ne_zero line 103
  6. theorem OAI.SmoothMobiusCorrection.factors_primeProduct line 106
  7. theorem OAI.SmoothMobiusCorrection.primeSet_primeProduct line 115
  8. theorem OAI.SmoothMobiusCorrection.primeProduct_injective line 127
  9. theorem OAI.SmoothMobiusCorrection.primeProduct_squarefree line 131
  10. theorem OAI.SmoothMobiusCorrection.primeProduct_primeSet line 135
  11. def OAI.SmoothMobiusCorrection.mobiusPrimeCoeff line 145
  12. theorem OAI.SmoothMobiusCorrection.mobiusPrimeCoeff_nonsquarefree line 148
  13. theorem OAI.SmoothMobiusCorrection.mobiusPrimeCoeff_primeProduct line 152
  14. theorem OAI.SmoothMobiusCorrection.mobiusPrimeCoeff_tsum line 162
  15. theorem OAI.SmoothMobiusCorrection.mobiusPrimeCoeff_euler line 178
  16. lemma OAI.SmoothMobiusCorrection.prime_norm_two_le line 193
  17. lemma OAI.SmoothMobiusCorrection.prime_norm_pos line 202
  18. def OAI.SmoothMobiusCorrection.primeNormPower line 206
  19. def OAI.SmoothMobiusCorrection.primeCharacterTerm line 208
  20. def OAI.SmoothMobiusCorrection.primeDensity line 211
  21. lemma OAI.SmoothMobiusCorrection.norm_primeNormPower line 213
  22. lemma OAI.SmoothMobiusCorrection.primeDensity_norm_le_one line 217
  23. lemma OAI.SmoothMobiusCorrection.primeCharacterTerm_norm_le line 227
  24. lemma OAI.SmoothMobiusCorrection.primeCharacterTerm_norm_lt_one line 237
  25. lemma OAI.SmoothMobiusCorrection.one_sub_ne_zero line 242
  26. lemma OAI.SmoothMobiusCorrection.correctionDenominator_ne_zero line 247
  27. def OAI.SmoothMobiusCorrection.correctionTerm line 256
  28. def OAI.SmoothMobiusCorrection.eulerCorrection line 262
  29. lemma OAI.SmoothMobiusCorrection.correctionTerm_factor line 265
  30. lemma OAI.SmoothMobiusCorrection.correctionFactor_ne_zero line 278
  31. lemma OAI.SmoothMobiusCorrection.correctionTerm_uniform_bound line 286
  32. lemma OAI.SmoothMobiusCorrection.prime_norm_series_summable line 317
  33. lemma OAI.SmoothMobiusCorrection.correctionTerm_summable line 328
  34. theorem OAI.SmoothMobiusCorrection.eulerCorrection_ne_zero line 334
  35. lemma OAI.SmoothMobiusCorrection.primeCharacterTerm_differentiable line 339
  36. lemma OAI.SmoothMobiusCorrection.correctionTerm_differentiableOn line 345
  37. lemma OAI.SmoothMobiusCorrection.eulerCorrection_locally_uniform line 358
  38. theorem OAI.SmoothMobiusCorrection.eulerCorrection_differentiableOn_halfplane line 368
  39. theorem OAI.SmoothMobiusCorrection.eulerCorrection_differentiableOn line 381
  40. lemma OAI.SmoothMobiusCorrection.prod_primeSet line 397
  41. lemma OAI.SmoothMobiusCorrection.primeValueHom_squarefree line 405
  42. lemma OAI.SmoothMobiusCorrection.outside_primeProduct_iff line 412
  43. def OAI.SmoothMobiusCorrection.outsideMask line 424
  44. lemma OAI.SmoothMobiusCorrection.prod_cut_primes line 427
  45. lemma OAI.SmoothMobiusCorrection.nat_cpow_prod line 441
  46. lemma OAI.SmoothMobiusCorrection.primeNormTerm_prod line 449
  47. def OAI.SmoothMobiusCorrection.ordinaryPrimeValue line 457
  48. def OAI.SmoothMobiusCorrection.dampedPrimeValue line 461
  49. def OAI.SmoothMobiusCorrection.ordinarySeriesTerm line 465
  50. def OAI.SmoothMobiusCorrection.dampedSeriesTerm line 469
  51. lemma OAI.SmoothMobiusCorrection.ordinarySeriesTerm_eq line 473
  52. lemma OAI.SmoothMobiusCorrection.dampedSeriesTerm_eq line 486
  53. lemma OAI.SmoothMobiusCorrection.ordinaryPrimeValue_norm_le line 506
  54. lemma OAI.SmoothMobiusCorrection.dampedPrimeValue_norm_le line 515
  55. lemma OAI.SmoothMobiusCorrection.prime_reciprocal_series_summable line 526
  56. lemma OAI.SmoothMobiusCorrection.ordinaryPrimeValue_summable line 531
  57. lemma OAI.SmoothMobiusCorrection.dampedPrimeValue_summable line 536
  58. lemma OAI.SmoothMobiusCorrection.ordinarySeries_euler line 541
  59. lemma OAI.SmoothMobiusCorrection.dampedSeries_euler line 548
  60. lemma OAI.SmoothMobiusCorrection.local_correction_identity line 555
  61. theorem OAI.SmoothMobiusCorrection.actual_dirichlet_correction line 568
  62. lemma OAI.SmoothMobiusCorrection.normFiber_tsum line 588
  63. lemma OAI.SmoothMobiusCorrection.idealDirichlet_fiber line 605
  64. lemma OAI.SmoothMobiusCorrection.idealDirichlet_summable line 621
  65. theorem OAI.SmoothMobiusCorrection.idealDirichlet_eq_LSeries line 629
  66. lemma OAI.SmoothMobiusCorrection.ordinarySeriesTerm_outside line 638
  67. lemma OAI.SmoothMobiusCorrection.dampedSeriesTerm_outside line 644
  68. lemma OAI.SmoothMobiusCorrection.ordinarySeries_eq_LSeries line 651
  69. lemma OAI.SmoothMobiusCorrection.dampedSeries_eq_LSeries line 663
  70. theorem OAI.SmoothMobiusCorrection.actual_LSeries_correction line 669
  71. theorem OAI.SmoothMobiusCorrection.full_LSeries_correction line 676
  72. theorem OAI.SmoothMobiusCorrection.eulerCorrection_analytic line 685