UniformCoordinateGeneration.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounded generation throughout the compact law family

A common local image ball and a finite set of schemes give common length and amplitude bounds on every fixed logarithmic ball. The scaling step uses only the exact straight-line one-parameter identity of each coordinate group.

theorem OAI.PolycyclicRecognition.exists_uniform_bounded_coordinate_words line 25

Source documentation

A fixed bounded coordinate ball is reached by generator words with bounds independent of the law in the compact normalized family.

theorem exists_uniform_bounded_coordinate_words {J : Type*} {c : ℕ}
    (a : DynkinCoefficients c 2) (b₀ : Basis J ℝ V) (w₀ : J → FreeMagma I)
    (C₀ R : ℝ) :
    ∃ (N : ℕ) (C : ℝ), 1 ≤ C ∧
      ∀ p ∈ normalizedExponentialParameters a w₀ b₀ C₀,
        ∀ v : V, ‖v‖ ≤ R → ∃ u : List (I × ℝ),
          u.length ≤ N ∧ (∀ z ∈ u, |z.2| ≤ C) ∧
            polynomialWord (dynkinProduct a p.1) p.2 u = v := by
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.normalizedExponentialParameters, OAI.PolycyclicRecognition.polynomialWord, OAI.PolycyclicRecognition.dynkinProduct