UniformShearingWindow.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform terminal shearing windows

The stopping-time estimate gives convergence uniformly throughout a terminal window whose relative length shrinks to zero. In particular, the error relative to the limiting shear lies in every identity neighborhood throughout that window.

lemma OAI.DukePrimeDegree.eventually_uniform_of_all_selections line 21
theorem OAI.DukePrimeDegree.root_conjugation_terminal_uniform line 45

theorem OAI.DukePrimeDegree.root_conjugation_terminal_error line 75

Source documentation

The small multiplying error in the pair-measure argument is uniformly close to identity over the entire window.

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

Mentions: OAI.DukePrimeDegree.rootShearSize