OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanLinkedProbeChains.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   All three logarithmic chains in the original neighboring-sheet coordinates. The first starts at the allowed suffix, the second at its neighbor, and the third starts at the second's actual last vertex. Their coefficients retain their original template bounds.

   structure LinkedProbeChains
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (E : Fin 3 → Set W) (γ : M.Bases) (t : Fin M.letterCount → ℝ) (scale : ℕ → ℝ)
       {Y : ℕ → Type*} [∀ n, MeasurableSpace (Y n)]
       (probe : Fin 3 → ∀ n, Y n → F.N.carrier)
       (P : ∀ k, M.BoxProbeChains T F hunimod eW b₀ (E k) γ t scale (probe k))
       (origin base : ∀ n, Y n → cartanRootIdeal H) (ε : ℕ → ℝ) where
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

2. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_linked_probe_chains line 59

   Source documentation

   Translate the two noninitial chains consecutively and keep one vanishing prefix envelope. In particular, the third initial profile is exactly the second terminal profile, rather than merely asymptotic to it.

   theorem exists_linked_probe_chains
       (haarN : NilpotentExponentialHaarInput F.N.modelSpace F.N.carrier)
       (dynkinN : NilpotentDynkinExpansionInput F.N.modelSpace F.N.carrier)
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (E : Fin 3 → Set W) (γ : M.Bases) (t : Fin M.letterCount → ℝ)
       (hγ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
         (fun w => bracketWordExponent t w) γ.val)
       (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop) (hscale1 : ∀ n, 1 ≤ scale n)
       {Y : ℕ → Type*} [∀ n, MeasurableSpace (Y n)]
       (probe : Fin 3 → ∀ n, Y n → F.N.carrier)
       (P : ∀ k, M.BoxProbeChains T F hunimod eW b₀ (E k) γ t scale (probe k))
       (origin base : ∀ n, Y n → cartanRootIdeal H)
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.bracketWordExponent

3. theorem OAI.PolycyclicRecognition.CartanWordModel.LinkedProbeChains.exp_eq_start_mul line 134

   Source documentation

   Each linked chain is the original chain left-translated by its actual initial vertex; this identity keeps the common profile centering unchanged.

   theorem LinkedProbeChains.exp_eq_start_mul
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (E : Fin 3 → Set W) (γ : M.Bases) (t : Fin M.letterCount → ℝ) (scale : ℕ → ℝ)
       {Y : ℕ → Type*} [∀ n, MeasurableSpace (Y n)]
       (probe : Fin 3 → ∀ n, Y n → F.N.carrier)
       (P : ∀ k, M.BoxProbeChains T F hunimod eW b₀ (E k) γ t scale (probe k))
       (origin base : ∀ n, Y n → cartanRootIdeal H) (ε : ℕ → ℝ)
       (Q : M.LinkedProbeChains T F hunimod eW b₀ E γ t scale probe P origin base ε)
       (k : Fin 3) (n : ℕ) (y : Y n) (j : Fin ((P k).length + 1)) :
       F.ExpN (F.N.equiv (Q.vertex k n y j)) =
         F.ExpN (F.N.equiv (Q.vertex k n y 0)) *
           F.ExpN (F.N.equiv ((P k).vertex n y j)) := by
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

4. theorem OAI.PolycyclicRecognition.CartanWordModel.LinkedProbeChains.endpoint line 159

   Source documentation

   The three last vertices are the actual three endpoints used in packing.

   theorem LinkedProbeChains.endpoint
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (E : Fin 3 → Set W) (γ : M.Bases) (t : Fin M.letterCount → ℝ) (scale : ℕ → ℝ)
       {Y : ℕ → Type*} [∀ n, MeasurableSpace (Y n)]
       (probe : Fin 3 → ∀ n, Y n → F.N.carrier)
       (P : ∀ k, M.BoxProbeChains T F hunimod eW b₀ (E k) γ t scale (probe k))
       (origin base : ∀ n, Y n → cartanRootIdeal H) (ε : ℕ → ℝ)
       (Q : M.LinkedProbeChains T F hunimod eW b₀ E γ t scale probe P origin base ε)
       (n : ℕ) (y : Y n) :
       F.ExpN (F.N.equiv (Q.vertex 0 n y (Fin.last (P 0).length))) =
         F.ExpN (F.N.equiv (origin n y)) * probe 0 n y ∧
       F.ExpN (F.N.equiv (Q.vertex 1 n y (Fin.last (P 1).length))) =
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal