ShearingWindow.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform control on a terminal shearing window

A quadratic displacement bounded up to its stopping time changes by at most a fixed multiple of the relative window length near that time. This is the quantitative algebra needed to replace a short orbit window by a single terminal shear in the measure argument.

lemma OAI.DukePrimeDegree.quadratic_sample_coefficient_bounds line 21
lemma OAI.DukePrimeDegree.quadratic_terminal_window_bound line 28

theorem OAI.DukePrimeDegree.root_conjugation_terminal_window line 53

Source documentation

Every matrix entry stays close to its terminal value on a short relative window, uniformly over all stopping times and nearby matrices.

theorem root_conjugation_terminal_window {n : ℕ} {i j : Fin n} (hij : i ≠ j)
    (g : G n) {T a : ℝ} (hT : 0 < T)
    (hbound : ∀ t ∈ Icc 0 T, rootShearSize hij g t ≤ a)
    (s : ℝ) (hs : s ∈ Icc (0 : ℝ) 1) (r q : Fin n) :
    |(Matrix.SpecialLinearGroup.transvection hij (s * T) * g *
        Matrix.SpecialLinearGroup.transvection hij (-(s * T))).val r q -
      (Matrix.SpecialLinearGroup.transvection hij T * g *
        Matrix.SpecialLinearGroup.transvection hij (-T)).val r q| ≤
      17 * a * (1 - s) := by
…

Mentions: OAI.DukePrimeDegree.rootShearSize

theorem OAI.DukePrimeDegree.root_conjugation_window_tendsto line 89

Source documentation

A relative window shrinking to the terminal time has the same matrix limit as the terminal shear, even though the stopping times may diverge.

theorem root_conjugation_window_tendsto {n : ℕ} {i j : Fin n} (hij : i ≠ j)
    (g : ℕ → G n) (T s : ℕ → ℝ) (a : ℝ)
    (hT : ∀ m, 0 < T m)
    (hbound : ∀ m, ∀ t ∈ Icc 0 (T m), rootShearSize hij (g m) t ≤ a)
    (hs : ∀ m, s m ∈ Icc (0 : ℝ) 1) (hslim : Tendsto s atTop (𝓝 1))
    (h : G n)
    (hlim : Tendsto (fun m => Matrix.SpecialLinearGroup.transvection hij (T m) * g m *
      Matrix.SpecialLinearGroup.transvection hij (-T m)) atTop (𝓝 h)) :
    Tendsto (fun m => Matrix.SpecialLinearGroup.transvection hij (s m * T m) * g m *
      Matrix.SpecialLinearGroup.transvection hij (-(s m * T m))) atTop (𝓝 h) := by
…

Mentions: OAI.DukePrimeDegree.rootShearSize