OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanBasepointGeometryOfBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_basepoint_geometry_of_factor_bounds line 41

   Source documentation

   Quantitative factor bounds imply the required two box inclusions. This assembly lemma is used with the already proved metric factor theorem.

   theorem exists_basepoint_geometry_of_factor_bounds
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (hφ : ∀ h : H, F.action (F.ExpD (F.D.equiv h)) =
         M.adjointGroupAutomorphism T F.N.equiv F.ExpN F.isExpN
           (by rw [← show chartN = F.ExpN from funext hchartN]; exact chartN.bijective) dynkinN h)
       {K : ℝ} (hK : 0 ≤ K)
       (hLip : ∀ x y, ‖(π x).toAdd - (π y).toAdd‖ ≤ K * dist x y)
       (X : I → H) (d : ℕ) (βD : WordBasisSelections X (boundedBracketWords d))
       (E : Set W) (hE : IsCompact E) (hne : E.Nonempty) (β : M.Bases)
       (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
         (M.boxCost T hunimod eW E) β.val)
       {lo : ℝ} (hlo : 0 < lo)
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.boundedBracketWords, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates