OAI/GroupTheory/PolycyclicRecognition/Analysis/SublinearSheetLimits.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.rescaled_profile_limits_eq_of_sublinear_sheet_distance line 17

   Source documentation

   This compares the actual two suffixes with the same center and chart. Only their source distance at the chosen chart point must be sublinear.

   theorem rescaled_profile_limits_eq_of_sublinear_sheet_distance
       {K : ℝ≥0} (J : ℕ → G → W) (hJ : ∀ n, LipschitzWith K (J n))
       (scale : ℕ → ℝ) (hscale : ∀ n, 0 < scale n)
       (x k l : ℕ → G) (chart : ℕ → Z → G) (z : ℕ → Z) (f g : W)
       (hf : Tendsto (fun n => rescaledMapProfile (J n) (x n) (k n)
         (Real.log (scale n)) (chart n) (z n)) atTop (𝓝 f))
       (hg : Tendsto (fun n => rescaledMapProfile (J n) (x n) (l n)
         (Real.log (scale n)) (chart n) (z n)) atTop (𝓝 g))
       (hnear : ∀ ε : ℝ, 0 < ε → ∀ᶠ n in atTop,
         dist (x n * k n * chart n (z n)) (x n * l n * chart n (z n)) ≤ ε * scale n) :
       f = g := by
   …

   Mentions: OAI.PolycyclicRecognition.rescaledMapProfile