CoordinateSchemeSubmersion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform local images for the actual normalized coordinate family

The endpoint differential is computed from exact coordinate-axis curves. Its columns form a basis at every limiting law, so the compact submersion theorem supplies a common image ball and finitely many schemes.

theorem OAI.PolycyclicRecognition.partial_fderiv_eq_basis line 26

Source documentation

The differential in the amplitude directions is determined by the coordinate-axis identities, without differentiating any group operations.

theorem partial_fderiv_eq_basis {n : ℕ}
    (f : P × (Fin n → ℝ) → V) (p : P) (b : Basis (Fin n) ℝ V)
    (hd : DifferentiableAt ℝ f (p, 0))
    (haxis : ∀ i s, f (p, Pi.single i s) = s • b i) (t : Fin n → ℝ) :
    fderiv ℝ f (p, 0) (0, t) = b.equivFun.symm t := by
…

theorem OAI.PolycyclicRecognition.exists_coordinate_submersive_scheme line 52

Source documentation

Every limiting normalized law admits a polynomial generator scheme with surjective amplitude differential at the identity.

theorem exists_coordinate_submersive_scheme {J : Type*} {c : ℕ}
    (a : DynkinCoefficients c 2) (B : V →L[ℝ] V →L[ℝ] V) (hB : IsLieBracket B)
    (hg : PolynomialGroupLaws (dynkinProduct a B))
    (hc : ExponentialConjugationLaw (dynkinProduct a B) B)
    (X : I → V) (b₀ : Basis J ℝ V) (w₀ : J → FreeMagma I)
    (hw₀ : ∀ j, evalBilinearWord B X (w₀ j) = b₀ j) :
    ∃ (w : Fin (finrank ℝ V) → List (I × ℝ)) (i : Fin (finrank ℝ V) → I),
      polynomialEndpointScheme a w i (B, X) 0 = 0 ∧
      Function.Surjective (fun t : Fin (finrank ℝ V) → ℝ =>
        fderiv ℝ (fun z => polynomialEndpointScheme a w i z.1 z.2) ((B, X), 0) (0, t)) := by
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.IsLieBracket, OAI.PolycyclicRecognition.PolynomialGroupLaws, OAI.PolycyclicRecognition.dynkinProduct, OAI.PolycyclicRecognition.ExponentialConjugationLaw, OAI.PolycyclicRecognition.evalBilinearWord, OAI.PolycyclicRecognition.polynomialEndpointScheme

theorem OAI.PolycyclicRecognition.exists_uniform_coordinate_schemes line 87

Source documentation

Compactness gives finitely many schemes and one common logarithmic image ball throughout the normalized exponential family.

theorem exists_uniform_coordinate_schemes {J : Type*} {c : ℕ}
    (a : DynkinCoefficients c 2) (b₀ : Basis J ℝ V) (w₀ : J → FreeMagma I) (C : ℝ) :
    ∃ (schemes : Finset ((Fin (finrank ℝ V) → List (I × ℝ)) ×
        (Fin (finrank ℝ V) → I))) (ε : ℝ), 0 < ε ∧
      ∀ p ∈ normalizedExponentialParameters a w₀ b₀ C,
        ∃ s ∈ schemes, ball (0 : V) ε ⊆
          (polynomialEndpointScheme a s.1 s.2 p) '' ball 0 1 := by
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.normalizedExponentialParameters, OAI.PolycyclicRecognition.polynomialEndpointScheme