OAI/NumberTheory/CubicMoment/Estimates/NormDenominatorMellin.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The norm denominator in the actual Poisson formula stays in its Mellin kernel. No real power is inserted into the prime coefficients.

  1. def OAI.CubicFirstMoment.normDenominatorMultiplier line 12
  2. def OAI.CubicFirstMoment.normDenominatorLogSchwartz line 18
  3. def OAI.CubicFirstMoment.normDenominatorMellinCoefficient line 23
  4. lemma OAI.CubicFirstMoment.normDenominatorMellinCoefficient_integrable line 27
  5. lemma OAI.CubicFirstMoment.normDenominatorLogSchwartz_apply line 32
  6. lemma OAI.CubicFirstMoment.normDenominatorLogSchwartz_eq_radial line 50
  7. lemma OAI.CubicFirstMoment.normDenominatorLogSchwartz_eq_annular line 58
  8. lemma OAI.CubicFirstMoment.normDenominatorFourier_seminorm_uniform line 66
  9. theorem OAI.CubicFirstMoment.normDenominatorMellinCoefficient_pointwise_rapidDecay line 96