OAI/GroupTheory/PolycyclicRecognition/Geometry/CenteredHeightError.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.centered_height_sublinear line 15

   Source documentation

   The same linear coefficient works after centering the coarse map at any fixed source point. Only the additive sublinear-error constant changes.

   theorem centered_height_sublinear
       (π : G →* Multiplicative W) (A : W →L[ℝ] W) (f : G → G)
       (hsub : ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ g,
         ‖(π (f g)).toAdd - A ((π g).toAdd)‖ ≤ ε * dist 1 g + B)
       (x : G) :
       ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ g,
         ‖(π ((f x)⁻¹ * f (x * g))).toAdd - A ((π g).toAdd)‖ ≤ ε * dist 1 g + B := by
   …

2. theorem OAI.PolycyclicRecognition.centered_coarse_lipschitz line 44

   Source documentation

   Centering also preserves the coarse Lipschitz constants exactly.

   theorem centered_coarse_lipschitz (f : G → G) {L C : ℝ}
       (hf : ∀ a b, dist (f a) (f b) ≤ L * dist a b + C) (x a b : G) :
       dist ((f x)⁻¹ * f (x * a)) ((f x)⁻¹ * f (x * b)) ≤ L * dist a b + C := by
   …

3. theorem OAI.PolycyclicRecognition.absolute_height_sublinear_of_centered_uniform line 53

   Source documentation

   Uniform centered height control supplies the absolute sublinear estimate used in representative independence.

   theorem absolute_height_sublinear_of_centered_uniform
       (π : G →* Multiplicative W) (A : W →L[ℝ] W) (f : G → G)
       (hsub : ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ x g,
         ‖(π ((f x)⁻¹ * f (x * g))).toAdd - A ((π g).toAdd)‖ ≤ ε * dist 1 g + B) :
       ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ g,
         ‖(π (f g)).toAdd - A ((π g).toAdd)‖ ≤ ε * dist 1 g + B := by
   …