ShearingHorosphere.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The horospherical shape of a normalized shearing limit

The limiting matrix differs from the identity only in the chosen row and column, with unchanged diagonal. Its displacement is nilpotent of order at most three. This is the precise horospherical direction used in EKL (2006), Section 4.2, equations (4.6)--(4.8).

def OAI.DukePrimeDegree.RootHorosphereShape line 21
lemma OAI.DukePrimeDegree.root_conjugation_pivot_trace line 24

theorem OAI.DukePrimeDegree.rootShearLimit_horospherical line 37

Source documentation

The off-root entries remain unchanged, and centrality forces the two pivot diagonal limits to equal one.

theorem rootShearLimit_horospherical {n : ℕ} {i j : Fin n} (hij : i ≠ j)
    (g : ℕ → G n) (hg : Tendsto g atTop (𝓝 1)) (t : ℕ → ℝ)
    (h : G n)
    (hlim : Tendsto (fun m => Matrix.SpecialLinearGroup.transvection hij (t m) * g m *
      Matrix.SpecialLinearGroup.transvection hij (-t m)) atTop (𝓝 h))
    (hcentral : h * Matrix.SpecialLinearGroup.transvection hij 1 =
      Matrix.SpecialLinearGroup.transvection hij 1 * h) : RootHorosphereShape i j h := by
…

Mentions: OAI.DukePrimeDegree.RootHorosphereShape

theorem OAI.DukePrimeDegree.rootHorosphereShape_nilpotent line 86
Source documentation
The displacement of a root-horospherical matrix has cube zero.
```
theorem rootHorosphereShape_nilpotent {n : ℕ} {i j : Fin n} (hij : i ≠ j)
    (g : G n) (hg : RootHorosphereShape i j g) :
    (g.val - 1) ^ 3 = 0 := by
…
```
Mentions: OAI.DukePrimeDegree.RootHorosphereShape

theorem OAI.DukePrimeDegree.exists_nontrivial_horospherical_rootShearLimit line 122

Source documentation

Normalized noncentral shearing produces a nonidentity unipotent horospherical limit.

theorem exists_nontrivial_horospherical_rootShearLimit
    {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 : ℝ} (ha : 0 < a)
    (hsize : ∀ m, rootShearSize hij (g m) (t m) = a)
    (hsmall : ∀ m, ∀ u ∈ Icc 0 (t m), rootShearSize hij (g m) u ≤ a) :
    ∃ h : G n, h ≠ 1 ∧ RootHorosphereShape i j h ∧ (h.val - 1) ^ 3 = 0 ∧
      ∃ φ : ℕ → ℕ, StrictMono φ ∧
        Tendsto (fun m => Matrix.SpecialLinearGroup.transvection hij (t (φ m)) * g (φ m) *
          Matrix.SpecialLinearGroup.transvection hij (-t (φ m))) atTop (𝓝 h) := by
…

Mentions: OAI.DukePrimeDegree.rootShearSize, OAI.DukePrimeDegree.RootHorosphereShape