OAI/NumberTheory/CubicMoment/Estimates/WideGramDecay.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Uniform Fourier decay for the fixed wider log-norm cutoff used by the actual prime convolution.

  1. lemma OAI.CubicFirstMoment.wideGramExp_deriv_bound line 12
  2. lemma OAI.CubicFirstMoment.wideGramExp_scale_growth line 29
  3. theorem OAI.CubicFirstMoment.schwartz_wideGramExp_comp_uniform line 41
  4. def OAI.CubicFirstMoment.wideGramBumpSchwartz line 86
  5. def OAI.CubicFirstMoment.wideAnnularLogSchwartz line 89
  6. lemma OAI.CubicFirstMoment.wideAnnularLogSchwartz_apply line 93
  7. lemma OAI.CubicFirstMoment.wideAnnularLogSchwartz_deriv_zero line 96
  8. theorem OAI.CubicFirstMoment.wideAnnularLogSchwartz_seminorm_uniform line 105
  9. theorem OAI.CubicFirstMoment.wideAnnularLogSchwartz_fourier_uniform line 152
  10. theorem OAI.CubicFirstMoment.wideAnnularLogSchwartz_fourier_L1_uniform line 181
  11. lemma OAI.CubicFirstMoment.wideAnnularLogSchwartz_eq_wideGramLogSchwartz line 203
  12. theorem OAI.CubicFirstMoment.wideGramMellinCoefficient_mass_rapidDecay line 213
  13. theorem OAI.CubicFirstMoment.wideGramMellinCoefficient_pointwise_rapidDecay line 229