OAI/NumberTheory/CubicMoment/Estimates/DivisorPoissonRadial.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact reindexing by the effective frequency d*h for a square-divisor Poisson block. The additive phase uses the actual inverse on the image.

  1. def OAI.CubicFirstMoment.divisorFourierPhase line 13
  2. lemma OAI.CubicFirstMoment.norm_divisorFourierPhase line 17
  3. lemma OAI.CubicFirstMoment.divisorFourierPhase_mul line 20
  4. def OAI.CubicFirstMoment.finiteDivisorPoissonContribution line 25
  5. theorem OAI.CubicFirstMoment.finiteDivisorPoissonContribution_radial line 32