OAI/NumberTheory/CubicGram/MellinNorm.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Mellin integral bounds for coprime radial forms.

  1. lemma OAI.CubicFirstMoment.gramMellinPhase_continuous line 17
  2. lemma OAI.CubicFirstMoment.gramMellinPhase_mul line 21
  3. lemma OAI.CubicFirstMoment.gramMellinCoefficient_integrable_phases line 26
  4. lemma OAI.CubicFirstMoment.thinDyad_mul line 37
  5. theorem OAI.CubicFirstMoment.radialDualProfile_twoRow_separated line 48
  6. def OAI.CubicFirstMoment.coprimeRadialForm line 61
  7. def OAI.CubicFirstMoment.coprimeNormMajorant line 68
  8. lemma OAI.CubicFirstMoment.coprimeNormMajorant_nonneg line 74
  9. lemma OAI.CubicFirstMoment.coprimeNormMajorant_phases line 83
  10. def OAI.CubicFirstMoment.coprimeMellinKernel line 93
  11. lemma OAI.CubicFirstMoment.coprimeMellinKernel_continuous line 100
  12. lemma OAI.CubicFirstMoment.norm_coprimeMellinKernel_le line 120
  13. theorem OAI.CubicFirstMoment.coprimeRadialForm_mellin line 137
  14. theorem OAI.CubicFirstMoment.coprimeRadialForm_norm_le line 197
  15. theorem OAI.CubicFirstMoment.coprimeRadialForm_rapidDecay line 230