OAI/GroupTheory/PolycyclicRecognition/Analysis/ProbeImageBridge.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.basedImage_bridge_product line 20

   Source documentation

   The product of the second path endpoint and the image bridge is the first probe endpoint in the same anchor frame.

   theorem basedImage_bridge_product (f : G → G) (a b c : G) :
       basedImage f a b * basedImage f b c = basedImage f a c := by
   …

   Mentions: OAI.PolycyclicRecognition.basedImage

2. theorem OAI.PolycyclicRecognition.rescaledMapProfile_basedImage line 26

   Source documentation

   The normalization used for counting probe images cancels from every raw height profile.

   theorem rescaledMapProfile_basedImage
       (height : G →* Multiplicative W) (f : G → G) (a x k : G)
       (r : ℝ) (chart : Z → G) (z : Z) :
       rescaledMapProfile (fun g => (height (basedImage f a g)).toAdd) x k r chart z =
         rescaledMapProfile (fun g => (height (f g)).toAdd) x k r chart z := by
   …

   Mentions: OAI.PolycyclicRecognition.rescaledMapProfile, OAI.PolycyclicRecognition.basedImage

3. theorem OAI.PolycyclicRecognition.basedImage_height_le_of_common_profile line 38

   Source documentation

   At the same Cartan coordinate the common affine profile gives a sublinear endpoint height, independently of its affine offset.

   theorem basedImage_height_le_of_common_profile
       (height : G →* Multiplicative W) (f : G → G)
       (x first second : G) (r : ℝ) (chart : Z → G)
       (q : Z → V) (A : V →ₗ[ℝ] W) (b : W) (z : Z)
       {ε₁ ε₂ : ℝ}
       (hfirst : ‖rescaledMapProfile (fun g => (height (f g)).toAdd) x first r chart z -
         (A (q z) + b)‖ ≤ ε₁)
       (hsecond : ‖rescaledMapProfile (fun g => (height (f g)).toAdd) x second r chart z -
         (A (q z) + b)‖ ≤ ε₂) :
       ‖(height (basedImage f (x * first * chart z) (x * second * chart z))).toAdd‖ ≤
         Real.exp r * (ε₁ + ε₂) := by
   …

   Mentions: OAI.PolycyclicRecognition.rescaledMapProfile, OAI.PolycyclicRecognition.basedImage

4. theorem OAI.PolycyclicRecognition.eventually_basedImage_height_small line 56

   Source documentation

   Vanishing profile error makes the same-coordinate endpoint height smaller than any fixed positive multiple of the geometric scale.

   theorem eventually_basedImage_height_small
       (height : G →* Multiplicative W) (f : ℕ → G → G)
       (x first second : ℕ → G) (scale ε : ℕ → ℝ) (chart : ℕ → Z → G)
       (q : Z → V) (A : V →ₗ[ℝ] W) (b : W) (z : ℕ → Z)
       (hscale : ∀ n, 0 < scale n) (hε : Tendsto ε atTop (𝓝 0))
       (hfirst : ∀ n, ‖rescaledMapProfile (fun g => (height (f n g)).toAdd)
         (x n) (first n) (Real.log (scale n)) (chart n) (z n) -
           (A (q (z n)) + b)‖ ≤ ε n)
       (hsecond : ∀ n, ‖rescaledMapProfile (fun g => (height (f n g)).toAdd)
         (x n) (second n) (Real.log (scale n)) (chart n) (z n) -
           (A (q (z n)) + b)‖ ≤ ε n)
       {δ : ℝ} (hδ : 0 < δ) :
   …

   Mentions: OAI.PolycyclicRecognition.rescaledMapProfile

5. theorem OAI.PolycyclicRecognition.basedImage_lipschitz line 83
6. theorem OAI.PolycyclicRecognition.dist_one_inv_mul_eq line 91

   Source documentation

   Left invariance identifies the bridge length with endpoint distance.

   theorem dist_one_inv_mul_eq (a b : G) : dist 1 (a⁻¹ * b) = dist a b := by
   …

7. theorem OAI.PolycyclicRecognition.basedImage_bridge_dist line 95

   Source documentation

   The actual image bridge has the Lipschitz-scaled source length.

   theorem basedImage_bridge_dist (f : G → G) {K : ℝ≥0} (hf : LipschitzWith K f)
       (a b : G) : dist 1 (basedImage f a b) ≤ (K : ℝ) * dist a b := by
   …

   Mentions: OAI.PolycyclicRecognition.basedImage

8. theorem OAI.PolycyclicRecognition.exists_uniform_bridge_parameter line 106

   Source documentation

   A single small source parameter works for every probe when the source bridge constants are uniform. No division by a possibly zero Lipschitz constant or bridge constant is used.

   theorem exists_uniform_bridge_parameter {K C D τ : ℝ}
       (hK : 0 ≤ K) (hC : 0 ≤ C) (hD : 0 ≤ D) (hτ : 0 < τ) :
       ∃ δ₀ : ℝ, 0 < δ₀ ∧ ∀ δ ε : ℝ, 0 ≤ δ → δ ≤ δ₀ →
         0 ≤ ε → ε ≤ δ₀ → K * (C * δ + D * ε) ≤ τ := by
   …

9. theorem OAI.PolycyclicRecognition.eventually_uniform_probe_height_small line 127

   Source documentation

   Profile agreement controls the endpoint heights uniformly over a retained family of probes, with one scale threshold for the whole family.

   theorem eventually_uniform_probe_height_small {J : ℕ → Type*}
       (height : G →* Multiplicative W) (f : ℕ → G → G)
       (x : ℕ → G) (first second : ∀ n, J n → G) (good : ∀ n, Set (J n))
       (scale ε : ℕ → ℝ) (chart : ℕ → Z → G)
       (q : Z → V) (A : V →ₗ[ℝ] W) (b : W) (z : ℕ → Z)
       (hscale : ∀ n, 0 < scale n) (hε : Tendsto ε atTop (𝓝 0))
       (hgood : ∀ᶠ n in atTop, ∀ j ∈ good n,
         ‖rescaledMapProfile (fun g => (height (f n g)).toAdd)
           (x n) (first n j) (Real.log (scale n)) (chart n) (z n) -
             (A (q (z n)) + b)‖ ≤ ε n ∧
         ‖rescaledMapProfile (fun g => (height (f n g)).toAdd)
           (x n) (second n j) (Real.log (scale n)) (chart n) (z n) -
   …

   Mentions: OAI.PolycyclicRecognition.rescaledMapProfile