OAI/NumberTheory/DukePrimeDegree/Dynamics/SingleBlockShearingLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A transverse limit from actual normalized return matrices

The shearing root, diverging first stopping times and transverse limit are all constructed. In particular, being outside the block group is a conclusion about the limit, not an additional hypothesis imposed on a subsequence.

  1. lemma OAI.DukePrimeDegree.slMatrixDifference_of_rootShearLimit line 22
  2. theorem OAI.DukePrimeDegree.exists_singleBlock_transverse_shearing_limit line 40