OAI/NumberTheory/DirichletL/Mellin/LogProfiles.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ShortDraftMellin.mobiusExpSum_continuousOn_pos line 13
  2. theorem OAI.ShortDraftMellin.mobiusExpSum_inv_continuousOn_pos line 65
  3. theorem OAI.ShortDraftMellin.mobiusExpSum_inv_locallyIntegrableOn_pos line 75
  4. theorem OAI.ShortDraftMellin.dirichlet_exp_zero_free_of_power_bound_only line 81
  5. theorem OAI.ShortDraftMellin.principal_dirichlet_exp_zero_free_of_power_bound_only line 91
  6. def OAI.ShortDraftMellin.ExponentialMobiusPowerBound line 145
  7. theorem OAI.ShortDraftMellin.dirichletTarget_of_exponentialMobiusPowerBound line 151
  8. theorem OAI.FiniteRingSieve.sum_chars_zero line 180
  9. theorem OAI.FiniteRingSieve.sum_chars line 187
  10. theorem OAI.FiniteRingSieve.unit_char_orthogonal line 199
  11. theorem OAI.FiniteRingSieve.complete_character_plancherel line 212
  12. theorem OAI.FiniteFieldSieve.complex_sum_cauchy line 261
  13. theorem OAI.FiniteFieldSieve.character_norm_le_one line 271
  14. theorem OAI.FiniteFieldSieve.primitive_gauss_norm_sq line 284
  15. theorem OAI.FiniteFieldSieve.gauss_shift_all line 297
  16. theorem OAI.FiniteFieldSieve.character_gauss_expansion line 309
  17. theorem OAI.FiniteFieldSieve.character_sum_le_additive_energy line 318
  18. def OAI.ProductResidueSieve.mulCharProd line 378
  19. def OAI.ProductResidueSieve.addCharProd line 389
  20. theorem OAI.ProductResidueSieve.mulCharProd_apply line 396
  21. theorem OAI.ProductResidueSieve.addCharProd_apply line 399
  22. theorem OAI.FourierBridge.schwartz_log_inversion line 411
  23. def OAI.FourierBridge.logProfile line 419
  24. theorem OAI.FourierBridge.logProfile_apply line 435
  25. theorem OAI.FourierBridge.smooth_log_separation line 442
  26. theorem OAI.FourierBridge.fourier_coefficient_moment line 453
  27. theorem OAI.FourierBridge.logProfile_coefficient_integrable line 461
  28. theorem OAI.FourierBridge.logProfile_coefficient_moment line 470
  29. theorem OAI.FourierBridge.logProfile_pointwise_decay line 484
  30. theorem OAI.FourierBridge.logProfile_zero_seminorm_decay line 513
  31. theorem OAI.FourierBridge.exp_argument_derivative_bound line 545
  32. theorem OAI.FourierBridge.coupled_factor_derivative_bound line 568
  33. theorem OAI.FourierBridge.derivative_scale_absorption line 590
  34. theorem OAI.FourierBridge.coupled_factor_uniform_derivative line 626
  35. theorem OAI.FourierBridge.logProfile_derivative_decay line 648
  36. theorem OAI.FourierBridge.logProfile_uniform_seminorm line 706
  37. theorem OAI.FourierBridge.fourier_seminorm_from_derivative_integrals line 789
  38. theorem OAI.FourierBridge.uniform_fourier_seminorm_transfer line 810
  39. theorem OAI.FourierBridge.uniform_fourier_coefficient_moment line 869
  40. def OAI.FourierBridge.profileDerivativeConstant line 908
  41. theorem OAI.FourierBridge.profileDerivativeConstant_nonneg line 913
  42. def OAI.FourierBridge.profileMomentConstant line 921
  43. theorem OAI.FourierBridge.profileMomentConstant_nonneg line 926
  44. theorem OAI.FourierBridge.profileMomentConstant_dominates line 935
  45. theorem OAI.FourierBridge.uniform_logProfile_source_pair line 951
  46. theorem OAI.FourierBridge.uniform_logProfile_coefficient_moment line 1030
  47. theorem OAI.FourierBridge.uniform_logProfile_coefficient_moment_explicit line 1070
  48. def OAI.FourierBridge.coefficientMomentBound line 1113
  49. theorem OAI.FourierBridge.coefficientMomentBound_nonneg line 1118
  50. theorem OAI.FourierBridge.uniform_fourier_one_plus_moment line 1123
  51. def OAI.FourierBridge.logPhase line 1188
  52. theorem OAI.FourierBridge.logPhase_add line 1191
  53. theorem OAI.FourierBridge.logPhase_zero line 1196
  54. theorem OAI.FourierBridge.logPhase_sum line 1199
  55. theorem OAI.FourierBridge.coupled_cutoff_active line 1207
  56. theorem OAI.FourierBridge.exists_complex_smooth_cutoff line 1228
  57. theorem OAI.FourierBridge.exists_complex_smooth_cutoff_with_derivative_bounds line 1269
  58. def OAI.FourierBridge.schwartzDerivativeDecayConstant line 1300
  59. theorem OAI.FourierBridge.schwartzDerivativeDecayConstant_nonneg line 1307
  60. theorem OAI.FourierBridge.schwartz_derivative_decay_finite line 1313
  61. theorem OAI.FourierBridge.coupled_log_separation line 1369
  62. theorem OAI.FourierBridge.coupled_log_coefficient_bound line 1425
  63. theorem OAI.FourierBridge.coupled_log_separation_schwartz line 1467