OAI/NumberTheory/CubicGram/MellinDecay.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Separated radial Mellin kernels with uniform rapid decay.

  1. def OAI.CubicFirstMoment.normProfileFourierSchwartz line 16
  2. lemma OAI.CubicFirstMoment.normProfileFourierSchwartz_apply line 21
  3. theorem OAI.CubicFirstMoment.radialDualProfile_rapidDecay line 30
  4. def OAI.CubicFirstMoment.gramLogBump line 60
  5. def OAI.CubicFirstMoment.gramLogKernel line 63
  6. lemma OAI.CubicFirstMoment.gramLogKernel_smooth line 66
  7. lemma OAI.CubicFirstMoment.gramLogKernel_compact line 79
  8. def OAI.CubicFirstMoment.gramLogSchwartz line 83
  9. lemma OAI.CubicFirstMoment.gramLogSchwartz_apply line 87
  10. lemma OAI.CubicFirstMoment.gramLogKernel_eq_radial line 91
  11. lemma OAI.CubicFirstMoment.gramLogKernel_dyad_ratio line 107
  12. def OAI.CubicFirstMoment.gramMellinCoefficient line 120
  13. def OAI.CubicFirstMoment.gramMellinPhase line 124
  14. lemma OAI.CubicFirstMoment.norm_gramMellinPhase line 127
  15. lemma OAI.CubicFirstMoment.gramMellinCoefficient_integrable line 130
  16. theorem OAI.CubicFirstMoment.radialDualProfile_mellin_separated line 135
  17. def OAI.CubicFirstMoment.gramExp line 174
  18. lemma OAI.CubicFirstMoment.gramExp_contDiff line 176
  19. lemma OAI.CubicFirstMoment.gramExp_deriv_bound line 179
  20. lemma OAI.CubicFirstMoment.gramExp_scale_growth line 196
  21. theorem OAI.CubicFirstMoment.schwartz_gramExp_comp_uniform line 208
  22. def OAI.CubicFirstMoment.gramBumpSchwartz line 252
  23. def OAI.CubicFirstMoment.annularLogSchwartz line 255
  24. lemma OAI.CubicFirstMoment.annularLogSchwartz_apply line 259
  25. lemma OAI.CubicFirstMoment.annularLogSchwartz_deriv_zero line 262
  26. theorem OAI.CubicFirstMoment.annularLogSchwartz_seminorm_uniform line 271
  27. theorem OAI.CubicFirstMoment.annularLogSchwartz_fourier_uniform line 318
  28. theorem OAI.CubicFirstMoment.annularLogSchwartz_fourier_L1_uniform line 347
  29. lemma OAI.CubicFirstMoment.annularLogSchwartz_eq_gramLogSchwartz line 369
  30. theorem OAI.CubicFirstMoment.gramMellinCoefficient_mass_rapidDecay line 379
  31. theorem OAI.CubicFirstMoment.gramMellinCoefficient_pointwise_rapidDecay line 395