OAI/GroupTheory/PolycyclicRecognition/Geometry/BoundedCenteredHeight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.bounded_family_height_of_centered_uniform line 12

   Source documentation

   On a family with bounded image centers, a uniform centered height estimate gives an uncentered estimate with one common additive constant.

   theorem bounded_family_height_of_centered_uniform
       {G W P : Type*} [Group G] [MetricSpace G]
       [NormedAddCommGroup W] [NormedSpace ℝ W]
       (π : G →* Multiplicative W) (A : W →L[ℝ] W) (f : G → G)
       {K : ℝ} (hK : 0 ≤ K)
       (hLip : ∀ x y, ‖(π x).toAdd - (π y).toAdd‖ ≤ K * dist x y)
       (hsub : ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ x g,
         ‖(π ((f x)⁻¹ * f (x * g))).toAdd - A ((π g).toAdd)‖ ≤ ε * dist 1 g + B)
       (center : P → G) {start : ℝ} (hstart : ∀ p, dist 1 (f (center p)) ≤ start) :
       ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ p g,
         ‖(π (f (center p * g))).toAdd - A ((π g).toAdd)‖ ≤ ε * dist 1 g + B := by
   …