OAI/NumberTheory/DukePrimeDegree/Dynamics/NoncentralReturns.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Noncentral neutral return matrices tending to identity

The proved nullity of exceptional return sets supplies arbitrarily small noncentral lifts on every positive-measure set. Choosing exponentially shrinking neighborhoods gives the sequence needed for shearing. Leaf-data equality along the neutral return is not assumed here.

  1. theorem OAI.DukePrimeDegree.exists_noncentral_neutral_return line 22
  2. lemma OAI.DukePrimeDegree.tendsto_one_of_shrinking_matrixBall line 40
  3. theorem OAI.DukePrimeDegree.exists_noncentral_neutral_return_sequence line 52