OAI/GroupTheory/PolycyclicRecognition/Analysis/SublinearScaleOffsets.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.uniform_sublinear_of_contractive_increments line 18

   Source documentation

   The scale-comparison estimate in the height argument forces its offsets to be uniformly sublinear. Only finitely many contractions are needed for each prescribed error, so no regularity of the offset as a function of scale is required.

   theorem uniform_sublinear_of_contractive_increments
       {P W : Type*} [NormedAddCommGroup W]
       (s : P → ℝ → W) {q C : ℝ} (hq : 0 < q) (hq1 : q < 1)
       (hbound : ∀ p r, 1 ≤ r → ‖s p r‖ ≤ C * r)
       (hincrement : ∀ ε : ℝ, 0 < ε → ∃ R : ℝ, 1 ≤ R ∧
         ∀ p r, R ≤ r → ‖s p r - s p (q * r)‖ ≤ ε * r) :
       ∀ ε : ℝ, 0 < ε → ∃ R : ℝ, 1 ≤ R ∧
         ∀ p r, R ≤ r → ‖s p r‖ ≤ ε * r := by
   …