ShearingCentralizer.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Centralizer limits of normalized shearing trajectories

Uniform control before the first shearing time bounds the quadratic coefficient. Since the shearing times diverge, the diagonal disturbance vanishes. Every convergent terminal matrix therefore lies in the root centralizer. These conclusions use actual special-linear matrices.

lemma OAI.DukePrimeDegree.root_conjugation_pivot line 21
lemma OAI.DukePrimeDegree.root_shearing_quadratic_bound line 30
lemma OAI.DukePrimeDegree.root_shearing_linear_bound line 52

lemma OAI.DukePrimeDegree.tendsto_root_shearing_linear_zero line 65

Source documentation

The diagonal perturbation tends to zero on a diverging normalized shearing interval.

lemma tendsto_root_shearing_linear_zero {n : ℕ} {i j : Fin n} (hij : i ≠ j)
    (g : ℕ → G n) (t : ℕ → ℝ) (ht : ∀ m, 0 < t m)
    (htop : Tendsto t atTop atTop) (a : ℝ)
    (hsmall : ∀ m, ∀ u ∈ Icc 0 (t m), rootShearSize hij (g m) u ≤ a) :
    Tendsto (fun m => t m * (g m).1 j i) atTop (𝓝 0) := by
…

Mentions: OAI.DukePrimeDegree.rootShearSize

theorem OAI.DukePrimeDegree.rootShearLimit_centralizes line 78

Source documentation

Every terminal limit of a uniformly bounded normalized shearing interval centralizes the original root subgroup.

theorem rootShearLimit_centralizes {n : ℕ} {i j : Fin n} (hij : i ≠ j)
    (g : ℕ → G n) (hg : Tendsto g atTop (𝓝 1))
    (t : ℕ → ℝ) (ht : ∀ m, 0 < t m) (htop : Tendsto t atTop atTop)
    (a : ℝ) (hsmall : ∀ m, ∀ u ∈ Icc 0 (t m), rootShearSize hij (g m) u ≤ a)
    (h : G n)
    (hlim : Tendsto (fun m => Matrix.SpecialLinearGroup.transvection hij (t m) * g m *
      Matrix.SpecialLinearGroup.transvection hij (-t m)) atTop (𝓝 h)) :
    ∀ u : ℝ, h * Matrix.SpecialLinearGroup.transvection hij u =
      Matrix.SpecialLinearGroup.transvection hij u * h := by
…

Mentions: OAI.DukePrimeDegree.rootShearSize