OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingSignedCentralizer.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Limits for shearing times of either sign

Annular return selection can produce positive or negative root times. Bounds on the symmetric interval and divergence of the absolute times suffice for the centralizer conclusion, without a sign assumption.

  1. lemma OAI.DukePrimeDegree.signed_root_shearing_quadratic_bound line 20
  2. lemma OAI.DukePrimeDegree.signed_root_shearing_linear_bound line 44
  3. lemma OAI.DukePrimeDegree.tendsto_signed_root_shearing_linear_zero line 55
  4. theorem OAI.DukePrimeDegree.rootShearLimit_signed_centralizes line 66