OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanPivotWordPath.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.CartanWordModel.pivotSupportFlow line 25
2. def OAI.PolycyclicRecognition.CartanWordModel.rootFlow line 29
3. def OAI.PolycyclicRecognition.CartanWordModel.pivotWordPath line 32
4. theorem OAI.PolycyclicRecognition.CartanWordModel.continuous_pivotWordPath_sample line 42
5. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_pivotWordPath_bound line 55

   Source documentation

   One constant bounds every explicitly prescribed word through the support positions. The word and its amplitudes may be chosen independently of the initial sheet.

   theorem exists_pivotWordPath_bound [IsIsometricSMul G G]
       (F : CartanFactorModel H Exp)
       (haarD : NilpotentExponentialHaarInput F.D.modelSpace F.D.carrier)
       (dynkinD : NilpotentDynkinExpansionInput F.D.modelSpace F.D.carrier)
       (π : G →* Multiplicative W)
       (hπ : ∀ x, (π (Exp x)).toAdd = eW (heightProjection T.character x))
       {E : Set W} (hE : Convex ℝ E) {w₀ : W} (hw₀ : w₀ ∈ E)
       (w : Fin M.letterCount → W) (hw : ∀ i, w i ∈ E)
       (s : Fin M.letterCount → ℝ)
       (hs : ∀ i, cartanHeightWeight T H (M.weight i) (eW.symm (w i)) = s i)
       {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (p N : ℕ) :
       ∃ C : ℝ, 0 ≤ C ∧ ∀ r : ℝ, 0 ≤ r → ∀ h₀ : H,
   …

   Mentions: OAI.PolycyclicRecognition.CartanFactorModel, OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.heightProjection, OAI.PolycyclicRecognition.cartanHeightWeight