OAI/GroupTheory/PolycyclicRecognition/Analysis/SequenceAccessiblePaths.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.sublinear_accessible_word_paths_sequence 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_sequence
       {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 : ℕ}
       (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop)
       (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)
   …

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