RescaledPivotLegs.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Compact coordinates for the actual pivot-to-support legs

theorem OAI.PolycyclicRecognition.exists_compact_rescaled_pivot_legs line 17

Source documentation

In a unit-cost word chart, the actual exponential leg from the pivot to each of finitely many support heights stays in one compact part of the open convex height domain. The coordinate identity is retained.

theorem exists_compact_rescaled_pivot_legs
    {L G W I J : Type*} [LieRing L] [LieAlgebra ℝ L] [Group G]
    [NormedAddCommGroup W] [NormedSpace ℝ W]
    [Fintype I] [DecidableEq I] [Fintype 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) (π : 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