OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanDilatedLinkedChains.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_dilated_linked_probe_chains line 32

   Source documentation

   Dilate all three normalized chains to the actual contact pivot, put all their prefixes in the enlarged sampling box, and attach the two original allowed suffixes. The produced linked chains retain the exact sampled group endpoints.

   theorem exists_dilated_linked_probe_chains
       (hbij : Function.Bijective F.ExpN)
       (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) (B C : Set W)
       (hE : ∀ k, IsCompact (E k)) (hne : ∀ k, (E k).Nonempty)
       (hB : IsCompact B) (hBne : B.Nonempty) (hC : IsCompact C)
       (w : W) (hBC : (fun x => x + w) '' B ⊆ C)
       (hw : ∀ i, 0 ≤ (M.supportIn T hunimod eW).weightSupport C i)
       (γ β : M.Bases)
       (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
   …

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