OAI/GroupTheory/PolycyclicRecognition/Analysis/AccessibleProfilePaths.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.accessible_word_profile_paths line 19

   Source documentation

   Successful parameters supply paths to every retained polynomial endpoint. The two good-sheet leg estimates and the short switch estimate control the whole image; subtracting the actual starting image costs its profile error.

   theorem accessible_word_profile_paths
       {L N G I W : Type*} [LieRing L] [LieAlgebra ℝ L] [Group N] [Group G]
       [PseudoMetricSpace G] [IsTopologicalGroup G]
       [NormedAddCommGroup W] [NormedSpace ℝ W] {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) (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 =
   …

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