RescaledWordPrefixes.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform coordinate bounds for every prefix of a bounded generator word

This is the prefix control needed to apply the neighboring-sheet argument to words supplied by uniform generation. Both the word length and the normalized amplitudes are bounded; the box shape and scale may vary.

theorem OAI.PolycyclicRecognition.exists_uniform_rescaled_word_prefix_bound line 28

Source documentation

Every prefix of every bounded normalized generator word remains in a single uniformly enlarged rescaled box.

theorem exists_uniform_rescaled_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 : I → ℝ)
      (β : WordBasisSelections X (boundedBracketWords c)),
      IsMaximizingColumnBasis (wordListCoordinates X (boundedBracketWords c) b₀)
        (fun w => bracketWordExponent s w) β.val →
…

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