DominatedWordPrefixes.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Bounded prefixes when a smaller template is used for generation

theorem OAI.PolycyclicRecognition.exists_uniform_dominated_word_prefix_bound line 21

Source documentation

Uniform generation in a smaller template does not force a change of the ambient maximizing basis. Shrinking each normalized letter amplitude places every prefix in a fixed-radius box for the larger template.

theorem exists_uniform_dominated_word_prefix_bound
    (dynkin : NilpotentDynkinExpansionInput E G)
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (X : I → L) {c : ℕ} (hc : lowerCentralSeries ℝ L L c = ⊥)
    (hletters : ∀ i : I, FreeMagma.of i ∈ boundedBracketWords c)
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L) (N : ℕ) {A : ℝ} (hA : 0 ≤ A) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (s t : I → ℝ), (∀ i, s i ≤ t i) →
      ∀ β : WordBasisSelections X (boundedBracketWords c),
      IsMaximizingColumnBasis (wordListCoordinates X (boundedBracketWords c) b₀)
        (fun w => bracketWordExponent t w) β.val →
      ∀ r : ℝ, 0 ≤ r → ∀ u : List (I × ℝ), u.length ≤ N →
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.boundedBracketWords, OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.bracketWordExponent