OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingLogTime.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Divergence of the logarithmic shearing window

Noncentral return matrices approaching the identity have positive scale tending to zero. Their logarithmic time window tends to infinity, and the two exponential regimes have exactly the bounds needed for the common-time selection theorem.

  1. lemma OAI.DukePrimeDegree.rootShearingKappa_one line 21
  2. def OAI.DukePrimeDegree.rootShearingLogTime line 34
  3. theorem OAI.DukePrimeDegree.rootShearingLogTime_normalizes line 37
  4. theorem OAI.DukePrimeDegree.rootShearingLogTime_nonneg line 47
  5. theorem OAI.DukePrimeDegree.rootShearingLogTime_tendsto line 55
  6. theorem OAI.DukePrimeDegree.rootShearingKappa_two_regimes line 72