OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingRegimes.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The two exponential shearing regimes

Over the logarithmic window, the inverse shearing scale is either fixed or decreases exponentially. Clamping the moving coefficient below its inactive threshold gives a single logarithmic parameter in [4*T,5*T], including when the original moving coefficient vanishes.

  1. lemma OAI.DukePrimeDegree.max_fixed_moving_clamp line 20
  2. theorem OAI.DukePrimeDegree.exists_two_exponential_shearing_regimes line 46