OAI/GroupTheory/PolycyclicRecognition/Geometry/SheetEndpointHeight.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.common_profile_endpoint_height line 16

   Source documentation

   At one chart point only the common limiting value matters. In particular, the offset and linear part of the affine profile cancel.

   theorem common_profile_endpoint_height
       {G W Z : Type*} [Group G] [NormedAddCommGroup W] [NormedSpace ℝ W]
       (J : G → W) (x k l d : G) (r : ℝ) (φ : Z → G) (z₀ : Z) (c : W)
       (hd : φ z₀ = d) {ε : ℝ}
       (hk : ‖rescaledMapProfile J x k r φ z₀ - c‖ ≤ ε)
       (hl : ‖rescaledMapProfile J x l r φ z₀ - c‖ ≤ ε) :
       ‖J (x * l * d) - J (x * k * d)‖ ≤ 2 * Real.exp r * ε := by
   …

   Mentions: OAI.PolycyclicRecognition.rescaledMapProfile

2. theorem OAI.PolycyclicRecognition.endpoint_height_of_short_bridges line 30

   Source documentation

   A short bridge at each endpoint adds twice its Lipschitz image to the endpoint height error. This is separate from control of the whole path.

   theorem endpoint_height_of_short_bridges
       {X W : Type*} [PseudoMetricSpace X] [NormedAddCommGroup W]
       (J : X → W) {K : ℝ≥0} (hJ : LipschitzWith K J)
       {a a' b' b : X} {δ B : ℝ}
       (ha : dist a a' ≤ δ) (hb : dist b' b ≤ δ)
       (hmid : ‖J b' - J a'‖ ≤ B) :
       ‖J b - J a‖ ≤ B + 2 * K * δ := by
   …