OAI/NumberTheory/CubicMoment/Estimates/DivisorNoncubeAnnulus.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Noncube saving for a literal square-divisor Poisson block. The principal condition is tested at d*h, as required by the character.

  1. theorem OAI.CubicFirstMoment.divisor_noncube_annulus_saving line 15