OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingTwoScales.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Preventing quadratic cancellation at two scales

This is the elementary cancellation step in EKL (2006), Section 4.5. A normalized quadratic root displacement is bounded away from zero either at a point of the first annulus or at every sufficiently large point of the second annulus.

  1. theorem OAI.DukePrimeDegree.normalized_quadratic_two_scales line 20