OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingScale.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A first scale for noncentral root shearing

Every matrix outside a root centralizer has a finite positive first time at which its conjugation displacement reaches a prescribed size. Before that time all matrix entries remain uniformly controlled. This is the stopping-time normalization used for the polynomial shearing argument.

  1. lemma OAI.DukePrimeDegree.continuous_first_level line 21
  2. def OAI.DukePrimeDegree.rootShearSize line 47
  3. lemma OAI.DukePrimeDegree.rootShearSize_zero line 51
  4. lemma OAI.DukePrimeDegree.continuous_rootShearSize line 55
  5. lemma OAI.DukePrimeDegree.entry_sub_le_rootShearSize line 70
  6. theorem OAI.DukePrimeDegree.exists_large_rootShearSize line 92

    Source documentation

    There is no bounded positive root-conjugation trajectory outside the root centralizer.

    theorem exists_large_rootShearSize {n : ℕ} {i j : Fin n} (hij : i ≠ j)
    (g : G n)
    (hnot : ¬ ∀ t : ℝ, g * Matrix.SpecialLinearGroup.transvection hij t =
      Matrix.SpecialLinearGroup.transvection hij t * g) (a : ℝ) :
    ∃ t : ℝ, 0 ≤ t ∧ a ≤ rootShearSize hij g t := by
…

    Mentions: OAI.DukePrimeDegree.rootShearSize

  7. theorem OAI.DukePrimeDegree.exists_first_rootShearScale line 125

    Source documentation

    A normalized finite shearing interval exists at every positive displacement scale for any noncentral matrix.

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

    Mentions: OAI.DukePrimeDegree.rootShearSize