UniformInteriorSlack.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Interior slack uniform in the sampled chart position

theorem OAI.PolycyclicRecognition.rescaled_word_conjugation_tendstoUniformly line 24

Source documentation

A common finite-word envelope gives uniform decay, even if the family parameter has no regularity. In particular it controls every compact set of sampled chart positions.

theorem rescaled_word_conjugation_tendstoUniformly
    {Z : Type*} [Nonempty (Fin (finrank ℝ L))]
    (X : I → L) {m k₀ c₀ : ℕ}
    (hk : lowerCentralSeries ℝ L L k₀ = ⊥)
    (hnil : lowerCentralSeries ℝ L L (m + 1) = ⊥)
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L)
    (s : I → ℝ)
    (β : ℝ → WordBasisSelections X (boundedBracketWords k₀))
    (hβ : ∀ r, IsMaximizingColumnBasis
      (wordListCoordinates X (boundedBracketWords k₀) b₀)
      (fun w => bracketWordExponent s w) (β r).val)
    (Exp : L → G) (hinj : Function.Injective Exp)
…

Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.boundedBracketWords, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.bracketWordExponent