OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanTiledProbeEndpoints.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.dilated_endpoints line 33

   Source documentation

   Dilation of the stored three samplers gives exactly the first endpoint, the selected second-sheet anchor, and the second endpoint.

   theorem TiledProbeChainData.dilated_endpoints
       (ExpI : M.coneWordIdeal C → I)
       (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (E : Fin 3 → Set W) (β : Fin 3 → M.ConeIdealBases C)
       (ambient : M.Bases) (t : Fin M.letterCount → ℝ) (scale : ℕ → ℝ)
       (φ : ℕ → I ≃ₜ* I) (ι : I →* F.N.carrier)
       (tiles : ℕ → ℕ) (anchor : ∀ n, Fin (tiles n) → I)
       (D : M.TiledProbeChainData T F hunimod eW C ExpI bN E β ambient t scale φ ι tiles anchor)
       (k : ℕ → F.N.carrier) (hφ : ∀ n z, ι (φ n z) = k n * ι z * (k n)⁻¹)
       (S : ℕ → MulAut F.N.carrier) (n : ℕ) (u : F.N.carrier)
       (y : (closedBall (0 : Fin (finrank ℝ
           (cartanRootIdeal H ⧸ (M.coneWordIdeal C).toSubmodule)) → ℝ) 1) ×
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal