CoordinateBoundedInverse.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounds for the continuous inverse schemes

The finite cover by inverse sections provides common bounds on expanded word length and on every amplitude, without a measurable-choice premise.

theorem OAI.PolycyclicRecognition.polynomialWord_generatorScheme_eq line 25
Source documentation
The direct word and the expanded endpoint polynomial agree for an actual polynomial coordinate group.
```
theorem polynomialWord_generatorScheme_eq {c n : ℕ}
    (a : DynkinCoefficients c 2) (B : V →L[ℝ] V →L[ℝ] V) (hB : IsLieBracket B)
    (hg : PolynomialGroupLaws (dynkinProduct a B)) (X : I → V)
    (w : Fin n → List (I × ℝ)) (i : Fin n → I) (t : Fin n → ℝ) :
    polynomialWord (dynkinProduct a B) X (generatorSchemeWord w i t) =
      polynomialEndpointScheme a w i (B, X) t :=
…
```
Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.IsLieBracket, OAI.PolycyclicRecognition.PolynomialGroupLaws, OAI.PolycyclicRecognition.dynkinProduct, OAI.PolycyclicRecognition.polynomialWord, OAI.PolycyclicRecognition.generatorSchemeWord, OAI.PolycyclicRecognition.polynomialEndpointScheme

theorem OAI.PolycyclicRecognition.exists_uniform_bounded_coordinate_inverse line 37

Source documentation

Every normalized law has one continuous bounded inverse scheme on a common ball; its expanded words have common length and amplitude bounds.

theorem exists_uniform_bounded_coordinate_inverse {J : Type*} {c : ℕ}
    (a : DynkinCoefficients c 2) (b₀ : Basis J ℝ V) (w₀ : J → FreeMagma I) (C₀ : ℝ) (n : ℕ) (hdim : finrank ℝ V = n) :
    ∃ (ε : ℝ) (N : ℕ) (C : ℝ), 0 < ε ∧ 1 ≤ C ∧
      ∀ p ∈ normalizedExponentialParameters a w₀ b₀ C₀,
        ∃ (w : Fin n → List (I × ℝ)) (i : Fin n → I)
          (σ : V → Fin n → ℝ),
          ContinuousOn σ (ball 0 ε) ∧ ∀ y ∈ ball (0 : V) ε,
            ‖σ y‖ < 1 ∧ (generatorSchemeWord w i (σ y)).length ≤ N ∧
            (∀ z ∈ generatorSchemeWord w i (σ y), |z.2| ≤ C) ∧
            polynomialWord (dynkinProduct a p.1) p.2 (generatorSchemeWord w i (σ y)) = y := by
…

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