OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingCompactness.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A nontrivial limit of normalized shearing

The normalized first shearing intervals provide bounded terminal matrices. Finite-dimensional compactness supplies a convergent subsequence, whose limit is nontrivial and centralizes the root group.

  1. def OAI.DukePrimeDegree.slMatrixDifference line 20
  2. lemma OAI.DukePrimeDegree.continuous_slMatrixDifference line 23
  3. lemma OAI.DukePrimeDegree.slMatrixDifference_self line 33
  4. theorem OAI.DukePrimeDegree.exists_nontrivial_rootShearLimit line 38

    Source documentation

    A normalized, bounded shearing sequence has a nonidentity subsequential limit in the root centralizer.

    theorem exists_nontrivial_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 ∧ ∃ φ : ℕ → ℕ, StrictMono φ ∧
      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