OAI/GroupTheory/PolycyclicRecognition/Geometry/LinkedRootProbeFrames.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PolycyclicRecognition.CartanWordModel.LinkedRootProbeFrames line 28

   Source documentation

   Retain the logarithmic chains together with the group equalities used by the measured comparison. The sampling domain stays an abstract parameter so that its coordinate construction is not repeated in every projection.

   structure LinkedRootProbeFrames
       {Y : ℕ → Type*} [∀ n, MeasurableSpace (Y n)]
       (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (E : Fin 3 → Set W) (γ : M.Bases) (width : Fin M.letterCount → ℝ)
       (scale : ℕ → ℝ) (probe : Fin 3 → ∀ n, Y n → F.N.carrier)
       (base step : ℕ → F.N.carrier)
       (first anchor second : ∀ n, Y n → F.N.carrier) where
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

2. theorem OAI.PolycyclicRecognition.CartanWordModel.LinkedRootProbeFrames.first_endpoint_distance_le line 60

   Source documentation

   Substitute the first endpoint before specializing the sampling domain. This keeps the metric comparison independent of its coordinate expressions.

   theorem LinkedRootProbeFrames.first_endpoint_distance_le
       (L : LinkedRootProbeFrames T M F hunimod eW bN E γ width scale probe base step
         first anchor second)
       (other : ∀ n, Y n → G) (tail : ℕ → G) (bound : ℕ → ℝ)
       (h : ∀ᶠ n in atTop, ∀ y, dist (other n y)
         (F.inclusionN (first n y) * tail n) ≤ bound n) :
       ∀ᶠ n in atTop, ∀ y, dist (other n y)
         (F.inclusionN (F.ExpN (F.N.equiv
           (L.linked.vertex 0 n y (Fin.last (L.chains 0).length)))) * tail n) ≤ bound n := by
   …

   Mentions: OAI.PolycyclicRecognition.CartanWordModel.LinkedRootProbeFrames