OAI/GroupTheory/PolycyclicRecognition/Geometry/ProfileChainHeightBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.relative_height_of_affine_profiles line 15

   Source documentation

   Different affine offsets are retained when comparing the two sheets.

   theorem relative_height_of_affine_profiles
       (J : G → W) (x k l : G) (r : ℝ) (φ : Z → G)
       (q : Z → V) (A : V →ₗ[ℝ] W) (b b₀ : W) (z z₀ : Z)
       {ε ε₀ : ℝ}
       (hz : ‖rescaledMapProfile J x k r φ z - (A (q z) + b)‖ ≤ ε)
       (hz₀ : ‖rescaledMapProfile J x l r φ z₀ - (A (q z₀) + b₀)‖ ≤ ε₀) :
       ‖J (x * k * φ z) - J (x * l * φ z₀) -
         Real.exp r • (A (q z - q z₀) + (b - b₀))‖ ≤ Real.exp r * (ε + ε₀) := by
   …

   Mentions: OAI.PolycyclicRecognition.rescaledMapProfile

2. theorem OAI.PolycyclicRecognition.relative_height_of_common_affine_profiles line 33

   Source documentation

   Two different sheets can be centered at the same original image. Their common affine offset cancels from the relative height estimate.

   theorem relative_height_of_common_affine_profiles
       (J : G → W) (x k l : G) (r : ℝ) (φ : Z → G)
       (q : Z → V) (A : V →ₗ[ℝ] W) (b : W) (z z₀ : Z)
       {ε ε₀ : ℝ}
       (hz : ‖rescaledMapProfile J x k r φ z - (A (q z) + b)‖ ≤ ε)
       (hz₀ : ‖rescaledMapProfile J x l r φ z₀ - (A (q z₀) + b)‖ ≤ ε₀) :
       ‖J (x * k * φ z) - J (x * l * φ z₀) -
         Real.exp r • A (q z - q z₀)‖ ≤ Real.exp r * (ε + ε₀) := by
   …

   Mentions: OAI.PolycyclicRecognition.rescaledMapProfile

3. theorem OAI.PolycyclicRecognition.chain_height_bound_of_common_affine_profile line 48

   Source documentation

   One common affine approximation to every prefix gives a uniform centered height bound over every permitted Cartan leg coordinate.

   theorem chain_height_bound_of_common_affine_profile
       {I : Type*} (J : G → W) (x : G) (suffix : I → G) (i₀ : I)
       (r : ℝ) (φ : Z → G) (q : Z → V) (A : V →ₗ[ℝ] W) (b : W)
       (Q : Set Z) (z₀ : Z) (hz₀ : z₀ ∈ Q) {ε : ℝ}
       (hgood : ∀ i z, z ∈ Q →
         ‖rescaledMapProfile J x (suffix i) r φ z - (A (q z) + b)‖ ≤ ε) :
       ∀ i z, z ∈ Q →
         ‖J (x * suffix i * φ z) - J (x * suffix i₀ * φ z₀) -
           Real.exp r • A (q z - q z₀)‖ ≤ 2 * Real.exp r * ε := by
   …

   Mentions: OAI.PolycyclicRecognition.rescaledMapProfile