OAI/GroupTheory/PolycyclicRecognition/Analysis/SublinearAccessiblePaths.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.sublinear_accessible_word_paths line 18

   Source documentation

   The vanishing good-profile errors on all support legs give exactly the relative height estimate required by the accessible-volume comparison. Only successful endpoints are used; the submersive endpoint map is unchanged.

   theorem sublinear_accessible_word_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 → ℝ) (letters : Fin m → I)
       (ι : N →* G) (hinj : Function.Injective ι) (x d₀ : ℝ → G)
       (A : ℝ → Set N) (n₀ : ℝ → N) (hn₀ : ∀ r, n₀ r ∈ A r)
       (sample : ℝ → ℕ → ℝ → N)
       (hsub : ∀ r j u v, sample r j u * (sample r j v)⁻¹ = sample r j (u - v))
   …

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