ConeIdealStrictWidth.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Strict width absorbs the inside-letter conjugation flow

The flow here is the finite exponential of the actual restricted adjoint. No box inclusion is an input. A positive width gap absorbs its polynomial growth uniformly over every point of the smaller box.

def OAI.PolycyclicRecognition.CartanWordModel.coneIdealLetterFlow line 23
theorem OAI.PolycyclicRecognition.CartanWordModel.exists_positive_coneIdeal_width line 26
theorem OAI.PolycyclicRecognition.CartanWordModel.norm_coneIdealBoxBasis_strict_width line 38

theorem OAI.PolycyclicRecognition.CartanWordModel.coneIdealLetterFlow_absorbed line 57

Source documentation

For a fixed strict width gap, all logarithmic conjugating times below the corresponding exponential threshold send the whole unit box into the larger unit box. Negative times are included.

theorem coneIdealLetterFlow_absorbed
    (b₀ : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C))
    (s : Fin M.letterCount → ℝ) (β : M.ConeIdealBases C)
    (hβ : M.IsMaximizingConeIdealBasis C b₀ s β)
    (i : Fin M.letterCount) (hi : s i = 0)
    {a b lo α : ℝ} (ha : 0 ≤ a) (hab : a < b) (hα : 0 ≤ α)
    (hlo : ∀ w : M.coneIdealWordList C, lo ≤ M.coneIdealWordCost C s w)
    (hgap : (M.bound : ℝ) * α < (b - a) * lo)
    (t ε : ℝ → ℝ) (hε : Tendsto ε atTop (𝓝 0))
    (ht : ∀ᶠ r in atTop, |t r| ≤ Real.exp ((α + ε r) * r)) :
    ∀ᶠ r in atTop, ∀ v : M.coneWordIdeal C,
      ‖(M.coneIdealBoxBasis C (fun j => a * s j) β r).equivFun v‖ ≤ 1 →
…