FixedTerminalShearing.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A fixed terminal fraction for every eventual shearing limit

The fraction is chosen using only the fixed displacement scale, the compact set of possible limits and the finite test family. It does not shrink along the sequence. Hence a previously chosen generic set gives valid control at the pair-dependent stopping times.

lemma OAI.DukePrimeDegree.slMatrixDifference_triangle line 22
lemma OAI.DukePrimeDegree.slMatrixDifference_le_of_entries line 31

theorem OAI.DukePrimeDegree.exists_fixed_terminal_observable_fraction line 45

Source documentation

The same fixed fraction works for all roots and every sequence with the specified bounded stopping intervals.

theorem exists_fixed_terminal_observable_fraction {n : ℕ}
    (F : Finset (CompactlySupportedContinuousMap (X n) ℝ))
    (K : Set (G n)) (hK : IsCompact K)
    (a ε : ℝ) (ha : 0 ≤ a) (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ δ < 1 ∧
      ∀ (i j : Fin n) (hij : i ≠ j)
        (g : ℕ → G n) (T : ℕ → ℝ),
        (∀ k, 0 < T k) →
        (∀ k, ∀ t ∈ Icc 0 (T k), rootShearSize hij (g k) t ≤ a) →
        ∀ h ∈ K,
          Tendsto (fun k => Matrix.SpecialLinearGroup.transvection hij (T k) * g k *
            Matrix.SpecialLinearGroup.transvection hij (-(T k))) atTop (𝓝 h) →
…

Mentions: OAI.DukePrimeDegree.rootShearSize