OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanBasisComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_groupBox_basis_comparison line 22

   Source documentation

   Replacing a selected word basis by a maximizing one costs a fixed multiplicative factor in the radius, uniformly in the template and scale.

   theorem exists_groupBox_basis_comparison
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H)) :
       ∃ C : ℝ, 1 ≤ C ∧ ∀ (E : Set W) (β γ : M.Bases),
         IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
           (M.boxCost T hunimod eW E) β.val →
         ∀ (r : ℝ), 0 ≤ r → ∀ {N : Type*} (exp : cartanRootIdeal H → N) (R : ℝ),
           M.groupBox T hunimod eW exp E γ r R ⊆
             M.groupBox T hunimod eW exp E β r (C * R) := by
   …

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