OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingSelectedConvergence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Convergence of the relative matrices at selected recurrence times

Any selection inside the logarithmic window preserves convergence to the identity. This justifies applying the signed shearing compactness argument after the recurrence time has been chosen.

  1. theorem OAI.DukePrimeDegree.rootPairConjugate_selected_tendsto_one line 20