GradedCoordinateLimit.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The limiting Lie law of maximizing word coordinates

def OAI.PolycyclicRecognition.gradedCoordinateBracket line 18

Source documentation

Retain exactly the structure constants which preserve total degree.

def gradedCoordinateBracket (b : Basis (Fin n) ℝ L) (cost : Fin n → ℝ) :
    (Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] (Fin n → ℝ) :=
…

theorem OAI.PolycyclicRecognition.rescaled_structureCoefficient_tendsto line 25

Source documentation

Each normalized structure constant converges; the strict-degree terms vanish and the degree-preserving terms stay unchanged.

theorem rescaled_structureCoefficient_tendsto
    (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)
    (i j k : Fin n) :
    Tendsto (fun r : ℝ => (exponentialRescaleBasis b cost r).repr
      ⁅exponentialRescaleBasis b cost r i, exponentialRescaleBasis b cost r j⁆ k)
      atTop (𝓝 (if cost i + cost j = cost k then b.repr ⁅b i, b j⁆ k else 0)) := by
…

Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis

theorem OAI.PolycyclicRecognition.basisBracket_rescale_tendsto line 47
Source documentation
Convergence holds in the finite-dimensional normed space of bilinear maps, so polynomial expressions in the group law converge on compacts.
```
theorem basisBracket_rescale_tendsto
    (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) :
    Tendsto (fun r : ℝ => basisBracket (exponentialRescaleBasis b cost r)) atTop
      (𝓝 (gradedCoordinateBracket b cost)) := by
…
```
Mentions: OAI.PolycyclicRecognition.basisBracket, OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.gradedCoordinateBracket
theorem OAI.PolycyclicRecognition.isLieBracket_gradedCoordinateBracket line 67
Source documentation
The limiting bilinear operation satisfies the Lie identities.
```
theorem isLieBracket_gradedCoordinateBracket
    (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) :
    IsLieBracket (gradedCoordinateBracket b cost) :=
…
```
Mentions: OAI.PolycyclicRecognition.IsLieBracket, OAI.PolycyclicRecognition.gradedCoordinateBracket

theorem OAI.PolycyclicRecognition.maximizing_word_basis_bracket_weight line 78

Source documentation

Maximality of the word-basis weight gives exactly the filtration inequality on every nonzero structure constant.

theorem maximizing_word_basis_bracket_weight
    (X : I → L) {k : ℕ} (hk : lowerCentralSeries ℝ L L 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)
    (i j l : Fin (finrank ℝ L))
    (hnz : (WordBasisSelections.basis X (boundedBracketWords k) β).repr
      ⁅WordBasisSelections.basis X (boundedBracketWords k) β i,
        WordBasisSelections.basis X (boundedBracketWords k) β j⁆ l ≠ 0) :
    bracketWordExponent s (β.val i) + bracketWordExponent s (β.val j) ≤
      bracketWordExponent s (β.val l) := by
…

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