OAI/NumberTheory/CubicMoment/Estimates/FinitePoissonRadial.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact identification of a finite Poisson frequency block with the radial form used in the Mellin estimates, including its scalar.

  1. def OAI.CubicFirstMoment.finitePoissonContribution line 14
  2. lemma OAI.CubicFirstMoment.poisson_scaled_sqrt line 20
  3. theorem OAI.CubicFirstMoment.finitePoissonContribution_radial line 27