OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingLimits.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Divergence of the normalized shearing time

For matrices approaching the identity, every time at which root conjugation has a fixed nonzero displacement tends to infinity. This places the stopping-time normalization on the scale required for the recurrence and leafwise comparison argument.

  1. lemma OAI.DukePrimeDegree.rootShearSize_one line 21
  2. lemma OAI.DukePrimeDegree.continuous_rootShearSize_pair line 26
  3. theorem OAI.DukePrimeDegree.rootShearScale_tendsto_atTop line 44
  4. theorem OAI.DukePrimeDegree.exists_diverging_first_rootShearScale line 69

    Source documentation

    Noncentral return matrices approaching the identity admit first shearing intervals whose lengths diverge.

    theorem exists_diverging_first_rootShearScale {n : ℕ} {i j : Fin n} (hij : i ≠ j)
    (g : ℕ → G n) (hg : Tendsto g atTop (𝓝 1))
    (hnot : ∀ m, ¬ ∀ t : ℝ, g m * Matrix.SpecialLinearGroup.transvection hij t =
      Matrix.SpecialLinearGroup.transvection hij t * g m)
    {a : ℝ} (ha : 0 < a) :
    ∃ t : ℕ → ℝ, Tendsto t atTop atTop ∧ ∀ m,
      0 < t m ∧ rootShearSize hij (g m) (t m) = a ∧
        ∀ u ∈ Icc 0 (t m), rootShearSize hij (g m) u ≤ a := by
…

    Mentions: OAI.DukePrimeDegree.rootShearSize