RescaledInverseSections.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Continuous endpoint coding in actual rescaled Lie coordinates

The compact normalized laws give a common coordinate ball and continuous inverse schemes. Transport through each actual rescaled basis preserves the endpoint identities and gives uniform bounds across all maximizing bases.

theorem OAI.PolycyclicRecognition.exists_uniform_rescaled_inverse_sections line 29

Source documentation

A continuous inverse generator scheme on one common ball in each actual rescaled logarithm chart. All constants are independent of scale, generator exponents, and maximizing word basis.

theorem exists_uniform_rescaled_inverse_sections (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)) :
    ∃ (ε : ℝ) (N : ℕ) (C : ℝ), 0 < ε ∧ 1 ≤ C ∧
…

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