CartanPivotWordImage.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Image bounds for the selected pivot word from its prefix sheets

The switch error is proved from the actual Cartan root curves. Only the finitely many outward and return sheet comparisons enter as hypotheses.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_pivotWordPath_observable_bound line 32

Source documentation

Once the profiles on the actual prefixes are close, their entire chosen path has the same height restriction, up to a logarithmic switch error. There is no assumption on profiles at unrelated sheets.

theorem exists_pivotWordPath_observable_bound
    (F : CartanFactorModel H Exp)
    (haarD : NilpotentExponentialHaarInput F.D.modelSpace F.D.carrier)
    (dynkinD : NilpotentDynkinExpansionInput F.D.modelSpace F.D.carrier)
    (π : G →* Multiplicative W)
    (hπ : ∀ x, (π (Exp x)).toAdd = eW (heightProjection T.character x))
    {E : Set W} (hE : Convex ℝ E) {w₀ : W} (hw₀ : w₀ ∈ E)
    (w : Fin M.letterCount → W) (hw : ∀ i, w i ∈ E)
    (s : Fin M.letterCount → ℝ)
    (hs : ∀ i, cartanHeightWeight T H (M.weight i) (eW.symm (w i)) = s i)
    {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (p N : ℕ) :
    ∃ Cp Cs : ℝ, 0 ≤ Cp ∧ 0 ≤ Cs ∧ ∀ r : ℝ, 0 ≤ r → ∀ h₀ : H,
…

Mentions: OAI.PolycyclicRecognition.CartanFactorModel, OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.heightProjection, OAI.PolycyclicRecognition.cartanHeightWeight