OAI/GroupTheory/PolycyclicRecognition/Analysis/AccessibleWordPaths.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.accessible_word_paths line 17

   Source documentation

   The successful parameter witnesses give paths to every point of the actual rescaled exponential image. No inverse to the polynomial endpoint map is chosen and no extra good-sheet hypothesis is introduced.

   theorem accessible_word_paths
       {L N G I : Type*} [LieRing L] [LieAlgebra ℝ L] [Group N] [Group G]
       [PseudoMetricSpace G] [IsTopologicalGroup G] {n m c : ℕ}
       (basis : Basis (Fin n) ℝ L) (Exp : L → N) (hzero : Exp 0 = 1)
       (a : DynkinCoefficients c 2)
       (hm : ∀ u v, Exp (finiteDynkinPolynomial a ![u, v]) = Exp u * Exp v)
       (X : I → L) (s : I → ℝ) (r : ℝ) (letters : Fin m → I)
       (ι : N →* G) (hinj : Function.Injective ι) (x d₀ : G)
       (A : Set N) (S : Set G) (n₀ : N) (hn₀ : n₀ ∈ A)
       (sample : ℕ → ℝ → N) (hsub : ∀ j u v, sample j u * (sample j v)⁻¹ = sample j (u - v))
       (hsample : ∀ j : Fin m, ∀ u, sample j.val u =
         Exp (u • (Real.exp (r * s (letters j)) • X (letters j))))
   …

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