RescaledLieFamily.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual rescalings lie in a compact family of normalized Lie laws

Both the law and the generator vectors are transported by the same rescaled word basis. Basis-word identities hold exactly, independently of the scale.

def OAI.PolycyclicRecognition.rescaledLieData line 23
Source documentation
The coordinate law and coordinate generators belonging to one rescaling.
```
def rescaledLieData (X : I → L) (S : Finset (FreeMagma I))
    (β : WordBasisSelections X S) (s : I → ℝ) (r : ℝ) :=
…
```
Mentions: OAI.PolycyclicRecognition.WordBasisSelections

theorem OAI.PolycyclicRecognition.rescaledLieData_word line 30

Source documentation

A selected rescaled word is exactly its coordinate unit vector.

theorem rescaledLieData_word (X : I → L) (S : Finset (FreeMagma I))
    (β : WordBasisSelections X S) (s : I → ℝ) (r : ℝ)
    (j : Fin (finrank ℝ L)) :
    evalBilinearWord (rescaledLieData X S β s r).1
      (rescaledLieData X S β s r).2 (β.val j) = Pi.single j 1 := by
…

Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.evalBilinearWord, OAI.PolycyclicRecognition.rescaledLieData

theorem OAI.PolycyclicRecognition.exists_rescaledLieData_bound line 53

Source documentation

A single bound works for all maximizing rescalings. For any fixed word basis, their closure is contained in the compact normalized parameter set.

theorem exists_rescaledLieData_bound (X : I → L) {k : ℕ}
    (hk : lowerCentralSeries ℝ L L k = ⊥)
    (hletters : ∀ i : I, FreeMagma.of i ∈ boundedBracketWords k)
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (s : I → ℝ)
      (β : WordBasisSelections X (boundedBracketWords k)),
      IsMaximizingColumnBasis (wordListCoordinates X (boundedBracketWords k) b₀)
        (fun w => bracketWordExponent s w) β.val →
      ∀ r : ℝ, 0 ≤ r →
      rescaledLieData X (boundedBracketWords k) β s r ∈
        normalizedLieParameters (fun j => (β.val j : FreeMagma I))
          (fun j => Pi.single j 1) C := by
…

Mentions: OAI.PolycyclicRecognition.boundedBracketWords, OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.bracketWordExponent, OAI.PolycyclicRecognition.rescaledLieData, OAI.PolycyclicRecognition.normalizedLieParameters

theorem OAI.PolycyclicRecognition.CartanWordModel.letter_mem_wordList line 85
Source documentation
Every actual Cartan letter occurs in the finite word list.
```
theorem letter_mem_wordList (M : CartanWordModel H) (i : Fin M.letterCount) :
    FreeMagma.of i ∈ M.wordList := by
…
```
Mentions: OAI.PolycyclicRecognition.CartanWordModel