RescaledUniformGeneration.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform generator words in the actual rescaled Lie model

The compact-family theorem is transported back through the actual coordinate bases. Finiteness of the word-basis choices gives bounds independent of the maximizing basis, scale, and generator exponents.

theorem OAI.PolycyclicRecognition.basis_polynomialWord line 22
Source documentation
Direct polynomial evaluation transports to the actual group word.
```
theorem basis_polynomialWord {n c : ℕ} (b : Basis (Fin n) ℝ L)
    (Exp : L → G) (hzero : Exp 0 = 1) (a : DynkinCoefficients c 2)
    (hm : ∀ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y)
    (X : I → L) (w : List (I × ℝ)) :
    Exp (b.equivFun.symm (polynomialWord (dynkinProduct a (basisBracket b))
      (fun i => b.equivFun (X i)) w)) = generatorGroupWord X Exp w := by
…
```
Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial, OAI.PolycyclicRecognition.polynomialWord, OAI.PolycyclicRecognition.dynkinProduct, OAI.PolycyclicRecognition.basisBracket, OAI.PolycyclicRecognition.generatorGroupWord

theorem OAI.PolycyclicRecognition.exists_uniform_rescaled_generator_words line 48

Source documentation

The actual rescaled boxes have generator-word bounds uniform over all exponents, nonnegative scales, and maximizing word bases.

theorem exists_uniform_rescaled_generator_words (X : I → L) {k : ℕ}
    (hk : lowerCentralSeries ℝ L L k = ⊥)
    (hletters : ∀ i : I, FreeMagma.of i ∈ boundedBracketWords k)
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L)
    (Exp : L → G) (hinj : Function.Injective Exp)
    (hzero : Exp 0 = 1) (hneg : ∀ x, Exp (-x) = (Exp x)⁻¹)
    (hadd : ∀ x (s t : ℝ), Exp ((s + t) • x) = Exp (s • x) * Exp (t • x))
    {c : ℕ} (a : DynkinCoefficients c 2)
    (hm : ∀ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y)
    (j : L →ₗ⁅ℝ⁆ A) (ρ : G →* Aˣ) (hρ : Function.Injective ρ)
    (hmatch : ∀ x, ρ (Exp x) = algebraExpUnit (j x)) (R : ℝ) :
    ∃ (N : ℕ) (C : ℝ), 1 ≤ C ∧ ∀ (s : I → ℝ)
…

Mentions: OAI.PolycyclicRecognition.boundedBracketWords, OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial, OAI.PolycyclicRecognition.algebraExpUnit