WordChartFlowHeight.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The exact height of a word-chart horizontal flow and its graded limit

theorem OAI.PolycyclicRecognition.wordChartFlow_height line 20

Source documentation

Exact height is retained at every finite physical scale.

theorem wordChartFlow_height (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)
    {r : ℝ} (hr : 1 ≤ r) (v : L) (z : Fin (finrank ℝ L) → ℝ) (t : ℝ) :
    let b := WordBasisSelections.basis X S β
…

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

theorem OAI.PolycyclicRecognition.gradedWordChartFlow_height line 51

Source documentation

The limiting horizontal flow projects to the original affine segment. This follows from convergence and the finite-scale identity, without an extra homomorphism premise on the limiting polynomial group.

theorem gradedWordChartFlow_height (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)
    (v : L) (z : Fin (finrank ℝ L) → ℝ) (t : ℝ)
    (hweight : ∀ i j k,
      (WordBasisSelections.basis X S β).repr
          ⁅(WordBasisSelections.basis X S β) i, (WordBasisSelections.basis X S β) j⁆ k ≠ 0 →
        bracketWordExponent (fun _ : I => 1) (β.val i) +
            bracketWordExponent (fun _ : I => 1) (β.val j) ≤
…