OAI/GroupTheory/PolycyclicRecognition/Analysis/ProbeImageGeometry.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.probe_image_two_path_geometry line 21

   Source documentation

   A finite image cover retains the witness needed to use the two actual paths. The second endpoint height is derived from its common affine profile; the image bridge is derived from the source bridge and the Lipschitz bound.

   theorem probe_image_two_path_geometry
       {Y : ℕ → Type*} (good : ∀ n, Set (Y n)) (tiles : ℕ → ℕ)
       (tile : ∀ n, Y n → Fin (tiles n)) (points : ∀ n, Fin (tiles n) → Finset G)
       (height : G →* Multiplicative W) (f : ℕ → G → G)
       (center base : ℕ → G) (anchor : ∀ n, Fin (tiles n) → G)
       (first second : ∀ n, Y n → G) (scale η : ℕ → ℝ)
       (chart : ℕ → Z → G) (q : Z → V) (z₀ : ℕ → Z)
       (A : V →ₗ[ℝ] W) (b : W) (E₁ E₂ : Set W)
       (L B δ D : ℝ) (Λ : ℝ≥0)
       (hscale : ∀ n, 0 < scale n) (hη : Tendsto η atTop (𝓝 0))
       (hδ : 0 < δ) (hLip : ∀ n, LipschitzWith Λ (f n)) (hD : (Λ : ℝ) * D ≤ δ)
       (hpoint : ∀ n j x, x ∈ points n j → ∃ y ∈ good n,
   …