OAI/NumberTheory/DukePrimeDegree/Dynamics/EqualLeafReturnWindows.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Equal-leaf return sequences with arbitrarily long shearing windows

Passing to a tail of the actual noncentral return sequence makes its scale at most one and its logarithmic window exceed any fixed bound. The common source set and equality of intrinsic leaves are preserved.

  1. theorem OAI.DukePrimeDegree.exists_equal_leaf_return_sequence_with_windows line 20