SublinearHeightComposition.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Composing the linear coefficients of sublinear height maps

theorem OAI.PolycyclicRecognition.two_point_sublinear_height_comp line 12

Source documentation

Uniform two-point sublinear errors compose. The coarse additive metric constant contributes only to the new additive height constant.

theorem two_point_sublinear_height_comp
    {X W : Type*} [PseudoMetricSpace X] [NormedAddCommGroup W] [NormedSpace ℝ W]
    (height : X → W) (f g : X → X) (A B : W →L[ℝ] W)
    {L C : ℝ} (hL : 0 ≤ L) (hC : 0 ≤ C)
    (hfLip : ∀ x y, dist (f x) (f y) ≤ L * dist x y + C)
    (hf : ∀ ε : ℝ, 0 < ε → ∃ D : ℝ, 0 ≤ D ∧ ∀ x y,
      ‖height (f y) - height (f x) - A (height y - height x)‖ ≤ ε * dist x y + D)
    (hg : ∀ ε : ℝ, 0 < ε → ∃ D : ℝ, 0 ≤ D ∧ ∀ x y,
      ‖height (g y) - height (g x) - B (height y - height x)‖ ≤ ε * dist x y + D) :
    ∀ ε : ℝ, 0 < ε → ∃ D : ℝ, 0 ≤ D ∧ ∀ x y,
      ‖height (g (f y)) - height (g (f x)) - (B.comp A) (height y - height x)‖ ≤
        ε * dist x y + D := by
…

theorem OAI.PolycyclicRecognition.sublinear_linear_height_error_of_close_to_id line 54

Source documentation

A map a bounded distance from the identity cannot have a different linear height coefficient modulo a sublinear two-point error.

theorem sublinear_linear_height_error_of_close_to_id
    {X W : Type*} [PseudoMetricSpace X] [NormedAddCommGroup W] [NormedSpace ℝ W]
    (height : X → W) (f : X → X) (A : W →L[ℝ] W)
    {K C : ℝ} (hK : 0 ≤ K) (hC : 0 ≤ C)
    (hheight : ∀ x y, ‖height x - height y‖ ≤ K * dist x y)
    (hclose : ∀ x, dist (f x) x ≤ C)
    (hf : ∀ ε : ℝ, 0 < ε → ∃ D : ℝ, 0 ≤ D ∧ ∀ x y,
      ‖height (f y) - height (f x) - A (height y - height x)‖ ≤ ε * dist x y + D) :
    ∀ ε : ℝ, 0 < ε → ∃ D : ℝ, 0 ≤ D ∧ ∀ x y,
      ‖(height y - height x) - A (height y - height x)‖ ≤ ε * dist x y + D := by
…

theorem OAI.PolycyclicRecognition.linear_height_coefficient_eq_id line 85

Source documentation

Actual linearly growing height rays identify a linear map whose height error is sublinear. This is used for the two coarse-inverse coefficients.

theorem linear_height_coefficient_eq_id
    {X W : Type*} [PseudoMetricSpace X] [NormedAddCommGroup W] [NormedSpace ℝ W]
    (base : X) (height : X → W) (A : W →L[ℝ] W) (ray : W → ℝ → X)
    (hray : ∀ w t, height (ray w t) - height base = t • w)
    (hmetric : ∀ w, ∃ L C : ℝ, 0 ≤ L ∧ ∀ t : ℝ, 0 ≤ t → dist base (ray w t) ≤ L * t + C)
    (hsub : ∀ ε : ℝ, 0 < ε → ∃ D : ℝ, ∀ x,
      ‖(height x - height base) - A (height x - height base)‖ ≤ ε * dist base x + D) :
    A = ContinuousLinearMap.id ℝ W := by
…