GradedGeneratorLimit.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Generating vectors and group laws survive the graded limit

def OAI.PolycyclicRecognition.gradedGenerator line 19
Source documentation
The part of a vector whose coordinate degree equals the prescribed generator degree.
```
def gradedGenerator {n : ℕ} (b : Basis (Fin n) ℝ L) (cost : Fin n → ℝ)
    (s : ℝ) (x : L) : Fin n → ℝ :=
…
```
theorem OAI.PolycyclicRecognition.rescaled_generator_tendsto line 23

theorem OAI.PolycyclicRecognition.maximizing_word_basis_letter_weight line 45

Source documentation

Basis maximality prevents a generator from having a nonzero coordinate of lower degree.

theorem maximizing_word_basis_letter_weight
    (X : I → L) (S : Finset (FreeMagma I)) (hletters : ∀ i, FreeMagma.of i ∈ S)
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L) (s : I → ℝ)
    (β : WordBasisSelections X S)
    (hβ : IsMaximizingColumnBasis (wordListCoordinates X S b₀)
      (fun w => bracketWordExponent s w) β.val)
    (i : I) (j : Fin (finrank ℝ L))
    (hnz : (WordBasisSelections.basis X S β).repr (X i) j ≠ 0) :
    s i ≤ bracketWordExponent s (β.val j) := by
…

Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.bracketWordExponent, OAI.PolycyclicRecognition.WordBasisSelections.basis

theorem OAI.PolycyclicRecognition.rescaledLieData_tendsto_graded line 66

Source documentation

The actual rescaled bracket and all actual generators converge together.

theorem rescaledLieData_tendsto_graded
    (X : I → L) {k : ℕ} (hk : lowerCentralSeries ℝ L L k = ⊥)
    (hletters : ∀ i : I, FreeMagma.of i ∈ boundedBracketWords k)
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L) (s : I → ℝ)
    (β : WordBasisSelections X (boundedBracketWords k))
    (hβ : IsMaximizingColumnBasis (wordListCoordinates X (boundedBracketWords k) b₀)
      (fun w => bracketWordExponent s w) β.val) :
    let b := WordBasisSelections.basis X (boundedBracketWords k) β
…

Mentions: OAI.PolycyclicRecognition.boundedBracketWords, OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.bracketWordExponent, OAI.PolycyclicRecognition.WordBasisSelections.basis

theorem OAI.PolycyclicRecognition.graded_generators_word_normalization line 88
Source documentation
Every selected bracket word still evaluates to its coordinate unit in the graded limit. Thus the limiting generators span the whole Lie algebra under brackets; the limit has not lost any directions.
```
theorem graded_generators_word_normalization
    (X : I → L) {k : ℕ} (hk : lowerCentralSeries ℝ L L k = ⊥)
    (hletters : ∀ i : I, FreeMagma.of i ∈ boundedBracketWords k)
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L) (s : I → ℝ)
    (β : WordBasisSelections X (boundedBracketWords k))
    (hβ : IsMaximizingColumnBasis (wordListCoordinates X (boundedBracketWords k) b₀)
      (fun w => bracketWordExponent s w) β.val) :
    let b := WordBasisSelections.basis X (boundedBracketWords k) β
…
```
Mentions: OAI.PolycyclicRecognition.boundedBracketWords, OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.bracketWordExponent, OAI.PolycyclicRecognition.WordBasisSelections.basis

theorem OAI.PolycyclicRecognition.gradedCoordinateBracket_groupLaws line 106

Source documentation

The fixed finite Dynkin product retains its exact group and straight-line one-parameter identities in the limiting coordinate law.

theorem gradedCoordinateBracket_groupLaws
    {G : Type*} [Group G] {n c : ℕ} (b : Basis (Fin n) ℝ L) (cost : Fin n → ℝ)
    (hweight : ∀ i j k, b.repr ⁅b i, b j⁆ k ≠ 0 → cost i + cost j ≤ cost k)
    (Exp : L → G) (hinj : Function.Injective Exp)
    (hzero : Exp 0 = 1) (hneg : ∀ x, Exp (-x) = (Exp x)⁻¹)
    (hadd : ∀ x (s t : ℝ), Exp ((s + t) • x) = Exp (s • x) * Exp (t • x))
    (a : DynkinCoefficients c 2)
    (hm : ∀ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y) :
    PolynomialGroupLaws (dynkinProduct a (gradedCoordinateBracket b cost)) :=
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial, OAI.PolycyclicRecognition.PolynomialGroupLaws, OAI.PolycyclicRecognition.dynkinProduct, OAI.PolycyclicRecognition.gradedCoordinateBracket