OAI/GroupTheory/PolycyclicRecognition/Geometry/RescaledHeightLegs.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_compact_rescaled_height_legs line 15

   Source documentation

   The physical scale version of compact pivot-leg control includes the pivot itself and retains the exact affine height of every selected point.

   theorem exists_compact_rescaled_height_legs
       {L G W I J : Type*} [LieRing L] [LieAlgebra ℝ L] [Group G]
       [NormedAddCommGroup W] [NormedSpace ℝ W]
       [Fintype I] [DecidableEq I] [Fintype J] [Nonempty J]
       (X : I → L) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
       (h : L →ₗ[ℝ] W) (hh : ∀ x y : L, h ⁅x, y⁆ = 0)
       (Exp : L → G) (hinj : Function.Injective Exp) (hzero : Exp 0 = 1)
       (π : G →* Multiplicative W) (hπ : ∀ x, (π (Exp x)).toAdd = h x)
       {c : ℕ} (a : DynkinCoefficients c 2)
       (hm : ∀ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y)
       (hweight : ∀ i j k,
         (WordBasisSelections.basis X S β).repr
   …

   Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial, OAI.PolycyclicRecognition.WordBasisSelections.basis