OAI/NumberTheory/CubicMoment/Angular/AngularHeightPoissonTail.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The complete absolute Poisson tail for angular coefficients, with unchanged coefficient energies and every frequency retained.

  1. theorem OAI.CubicFirstMoment.angular_logarithmic_absolute_poisson_dyad line 16
  2. theorem OAI.CubicFirstMoment.angular_logarithmic_poisson_tail line 58
  3. theorem OAI.CubicFirstMoment.angular_high_poisson_log_saving line 95