OAI/NumberTheory/DukePrimeDegree/Dynamics/TwoAnnularReturns.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compact returns in both normalized annuli

The synchronized small central portions and the intrinsic maximal estimate give simultaneous compact returns at both radii. Multiplying the chosen times by the shearing scale places them in the two annuli required by the polynomial noncancellation estimate.

  1. theorem OAI.DukePrimeDegree.exists_two_normalized_annular_returns line 22