OAI/GroupTheory/PolycyclicRecognition/Algebra/CoordinateConjugationDecay.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.coordinate_conjugation_tendsto_zero line 20

   Source documentation

   A sufficiently large exponential margin survives conjugation by every expanded-box coordinate, uniformly over a bounded family of actual brackets. The exact exponential-conjugation law is provided by the existing faithful realization theorem in the application.

   theorem coordinate_conjugation_tendsto_zero
       {L : Type*} [LieRing L] [LieAlgebra ℝ L] {n m c : ℕ}
       [Nonempty (Fin n)]
       (b : ℝ → Basis (Fin n) ℝ L)
       (hk : lowerCentralSeries ℝ L L (m + 1) = ⊥)
       (a : DynkinCoefficients c 2)
       (hconj : ∀ r, ExponentialConjugationLaw
         (dynkinProduct a (basisBracket (b r))) (basisBracket (b r)))
       (k y : ℝ → Fin n → ℝ)
       {C A B α β : ℝ} (hC : 0 ≤ C) (hA : 0 ≤ A) (hB : 0 ≤ B) (hα : 0 ≤ α)
       (hbound : ∀ᶠ r : ℝ in atTop, ‖basisBracket (b r)‖ ≤ C)
       (hgap : (m : ℝ) * α < β)
   …

   Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.ExponentialConjugationLaw, OAI.PolycyclicRecognition.dynkinProduct, OAI.PolycyclicRecognition.basisBracket