OAI/GroupTheory/PolycyclicRecognition/Geometry/ExponentialBoxRadius.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.norm_double_scale_le_one line 15

   Source documentation

   Doubling the scale absorbs a radius exp (r ε) whenever every coordinate cost is at least ε.

   theorem norm_double_scale_le_one
       {L J : Type*} [LieRing L] [LieAlgebra ℝ L] [Fintype J]
       (b : Basis J ℝ L) (cost : J → ℝ) {r ε : ℝ} (hr : 0 ≤ r)
       (hcost : ∀ j, ε ≤ cost j) (v : L)
       (hv : ‖(exponentialRescaleBasis b cost r).equivFun v‖ ≤ Real.exp (r * ε)) :
       ‖(exponentialRescaleBasis b cost (2 * r)).equivFun v‖ ≤ 1 := by
   …

   Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis