OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanChartAction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_chart_adjoint_word_envelope line 26

   Source documentation

   Every bounded set of scaled Cartan chart coordinates whose unscaled heights lie in the interior template has the required uniform word envelope. Polynomial logarithm control and exact height scaling are derived, rather than additional hypotheses.

   theorem exists_chart_adjoint_word_envelope
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       {E : Set W} (hE : IsCompact E) (hne : E.Nonempty) {t : ℝ} (ht : 0 ≤ t)
       (β γ : M.Bases)
       (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
         (M.boxCost T hunimod eW E) β.val)
       (X : I → H) (S : Finset (FreeMagma I)) (βD : WordBasisSelections X S)
       (z : Z → Fin (finrank ℝ H) → ℝ) {R : ℝ} (hR : 0 ≤ R)
       (hz : ∀ a, ‖z a‖ ≤ R)
       (hdomain : ∀ a, eW (heightProjection T.character
         ((WordBasisSelections.basis X S βD).equivFun.symm (z a) : L)) ∈
           (fun x => t • x) '' E)
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.heightProjection, OAI.PolycyclicRecognition.WordBasisSelections.basis