OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanUniformAction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_uniform_adjoint_word_envelope line 24

   Source documentation

   Polynomial control of the sampled Cartan logarithms makes the word coefficient error subexponential, uniformly over all chart positions.

   theorem exists_uniform_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)
       (h : ℝ → Z → H) (w : ℝ → Z → W)
       (hw : ∀ r, 1 ≤ r → ∀ z, w r z ∈ (fun x => t • x) '' E)
       (hh : ∀ r, 1 ≤ r → ∀ z,
         eW (heightProjection T.character (h r z : L)) = r • w r z)
       {B : ℝ} (hB : 0 ≤ B) (q : ℕ)
       (hlog : ∀ r, 1 ≤ r → ∀ z,
   …

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