RootShearing.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Polynomial shearing along a root subgroup

The exact matrix formula is the algebraic part of the low-entropy argument: conjugation by a root unipotent is quadratic in its parameter. The exceptional case is precisely the centralizer, and commuting with a single nonzero root element already characterizes that case.

lemma OAI.DukePrimeDegree.root_left_mul_entry line 21

theorem OAI.DukePrimeDegree.root_conjugation_entry line 32

Source documentation

The quadratic root-shearing formula, for arbitrary matrix indices.

theorem root_conjugation_entry {n : ℕ} {i j : Fin n} (hij : i ≠ j)
    (g : G n) (r s : Fin n) (t : ℝ) :
    (Matrix.SpecialLinearGroup.transvection hij t * g *
      Matrix.SpecialLinearGroup.transvection hij (-t)).1 r s =
      g.1 r s + (if r = i then t * g.1 j s else 0) -
        (if s = j then t * g.1 r i else 0) -
        (if r = i ∧ s = j then t ^ 2 * g.1 j i else 0) := by
…

theorem OAI.DukePrimeDegree.commutes_root_one_iff line 46

Source documentation

A matrix centralizes the entire root group exactly when its pivot column, pivot row and two diagonal entries satisfy these equations.

theorem commutes_root_one_iff {n : ℕ} {i j : Fin n} (hij : i ≠ j) (g : G n) :
    g * Matrix.SpecialLinearGroup.transvection hij 1 =
      Matrix.SpecialLinearGroup.transvection hij 1 * g ↔
      (∀ r, r ≠ i → g.1 r i = 0) ∧
      (∀ s, s ≠ j → g.1 j s = 0) ∧ g.1 i i = g.1 j j := by
…

theorem OAI.DukePrimeDegree.commutes_root_one_iff_all line 82

Source documentation

The centralizer of a root element at parameter one is the centralizer of the full real root subgroup.

theorem commutes_root_one_iff_all {n : ℕ} {i j : Fin n} (hij : i ≠ j) (g : G n) :
    g * Matrix.SpecialLinearGroup.transvection hij 1 =
      Matrix.SpecialLinearGroup.transvection hij 1 * g ↔
      ∀ t : ℝ, g * Matrix.SpecialLinearGroup.transvection hij t =
        Matrix.SpecialLinearGroup.transvection hij t * g := by
…

lemma OAI.DukePrimeDegree.bounded_quadratic_constant line 105
Source documentation
A quadratic polynomial bounded on the positive half-line is constant. This version keeps the exact coefficients used in shearing.
```
lemma bounded_quadratic_constant (a b c B : ℝ)
    (hbound : ∀ t : ℝ, 0 ≤ t → |a + b * t + c * t ^ 2| ≤ B) :
    ∀ t : ℝ, a + b * t + c * t ^ 2 = a := by
…
```

theorem OAI.DukePrimeDegree.commutes_root_of_bounded_conjugation line 123

Source documentation

A root-conjugation trajectory stays bounded for all positive times only in the exceptional, centralizing case.

theorem commutes_root_of_bounded_conjugation {n : ℕ} {i j : Fin n}
    (hij : i ≠ j) (g : G n) (B : ℝ)
    (hbound : ∀ t : ℝ, 0 ≤ t → ∀ r s : Fin n,
      |(Matrix.SpecialLinearGroup.transvection hij t * g *
        Matrix.SpecialLinearGroup.transvection hij (-t)).1 r s| ≤ B) :
    ∀ t : ℝ, g * Matrix.SpecialLinearGroup.transvection hij t =
      Matrix.SpecialLinearGroup.transvection hij t * g := by
…