OAI/GroupTheory/PolycyclicRecognition/Analysis/RescaledProbeChains.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_probe_translated_rescaled_chain line 21

   Source documentation

   A tile anchor may depend on the probe. Uniform box bounds for those anchors still give one vanishing envelope for all translated prefixes, and the exact generator edges are preserved.

   theorem exists_probe_translated_rescaled_chain
       (dynkin : NilpotentDynkinExpansionInput E G)
       (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
       (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
       (X : I → L) {c : ℕ} (hc : lowerCentralSeries ℝ L L c = ⊥)
       (b₀ : Basis (Fin (finrank ℝ L)) ℝ L)
       (s : I → ℝ) (β : WordBasisSelections X (boundedBracketWords c))
       (hβ : IsMaximizingColumnBasis (wordListCoordinates X (boundedBracketWords c) b₀)
         (fun w => bracketWordExponent s w) β.val)
       (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop) (hscale1 : ∀ n, 1 ≤ scale n)
       (ε₁ ε₂ : ℕ → ℝ) (hε₁0 : ∀ n, 0 ≤ ε₁ n) (hε₂0 : ∀ n, 0 ≤ ε₂ n)
       (hε₁ : Tendsto ε₁ atTop (𝓝 0)) (hε₂ : Tendsto ε₂ atTop (𝓝 0))
   …

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