OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanActionCoefficients.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   Containment of the Cartan height in a homothetic template gives an actual word expansion of the conjugated logarithm. Its only loss is a fixed polynomial in the Cartan logarithm, with the template exponent retained for each individual word.

   theorem exists_adjoint_word_coefficient_bound
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H)) :
       ∃ (A : ℝ) (p : ℕ), 0 ≤ A ∧ ∀ {E : Set W}, IsCompact E → E.Nonempty →
         ∀ {t : ℝ}, 0 ≤ t → ∀ (β : M.Bases),
         IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
           (M.boxCost T hunimod eW E) β.val →
         ∀ (γ : M.Bases) (r : ℝ), 0 ≤ r → ∀ (h : H) (w : W),
         w ∈ (fun x => t • x) '' E →
         eW (heightProjection T.character (h : L)) = r • w →
         ∀ v : cartanRootIdeal H, ∃ a : M.wordList → ℝ,
           (∀ u, |a u| ≤ A * (1 + ‖(Module.finBasis ℝ H).equivFun h‖) ^ p *
             ‖(WordBasisSelections.basis M.letter M.wordList γ).equivFun v‖ *
   …

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