OAI/NumberTheory/CubicMoment/Estimates/OuterPoissonAnnulus.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual coprime Poisson annulus, including cube frequencies, for the compact norm interval of a common-factor quotient.

  1. theorem OAI.CubicFirstMoment.coprime_poisson_outer_annulus line 14