OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingBoundedLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bounded shearing intervals with a positive terminal displacement

A selected annular return need not be the first time a prescribed level is attained. Uniform control of its preceding interval and a positive lower terminal bound suffice for the same nontrivial horospherical limit.

  1. theorem OAI.DukePrimeDegree.exists_bounded_horospherical_rootShearLimit line 20