OAI/GroupTheory/PolycyclicRecognition/Analysis/MixedScaleBasisBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.norm_exponentialRescaleBasis_le_of_exponents_le line 11

   Source documentation

   Only the products of physical scale and word cost matter for a box.

   theorem norm_exponentialRescaleBasis_le_of_exponents_le
       {L J : Type*} [LieRing L] [LieAlgebra ℝ L] [Fintype J]
       (b : Basis J ℝ L) (u v : J → ℝ) (r t : ℝ)
       (h : ∀ j, t * v j ≤ r * u j) (x : L) :
       ‖(exponentialRescaleBasis b u r).equivFun x‖ ≤
         ‖(exponentialRescaleBasis b v t).equivFun x‖ := by
   …

   Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis