CartanTiledLinkedEndpoints.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Exact endpoints of the counted sampler after dilation

theorem OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.linked_endpoints line 35

Source documentation

The logarithmic prefixes selected by concentration have exactly the three group endpoints used by the source count and the two image paths.

theorem TiledProbeChainData.linked_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 u : ℕ → F.N.carrier) (hφ : ∀ n z, ι (φ n z) = k n * ι z * (k n)⁻¹)
    (S : ℕ → MulAut F.N.carrier)
    {Y : ℕ → Type*} [∀ n, MeasurableSpace (Y n)]
    (ψ : ∀ n, Y n →
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal