DynkinWords.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Bounded finite Dynkin expansions

The analytic BCH input is separated from its elementary coordinate estimate. A degree-c expansion in right-nested words, with uniformly bounded coefficients, has polynomial growth in the number of input factors.

def OAI.PolycyclicRecognition.rightNestedWord line 20

Source documentation

A right-nested bracket in a nonempty ordered list of letters.

def rightNestedWord {I : Type*} : (d : ℕ) → (Fin (d + 1) → I) → FreeMagma I
  | 0, f => .of (f 0)
  | d + 1, f => .of (f 0) * rightNestedWord d (fun i => f i.succ)

theorem OAI.PolycyclicRecognition.rightNestedWord_nodes line 24
theorem OAI.PolycyclicRecognition.rightNestedWord_length line 30
abbrev OAI.PolycyclicRecognition.DynkinCoefficients line 34
def OAI.PolycyclicRecognition.finiteDynkinPolynomial line 39
Source documentation
A finite expansion of degree at most c in n input logarithms.
```
def finiteDynkinPolynomial {c n : ℕ} (coeff : DynkinCoefficients c n) (X : Fin n → L) : L :=
…
```
Mentions: OAI.PolycyclicRecognition.DynkinCoefficients

theorem OAI.PolycyclicRecognition.finiteDynkinPolynomial_map line 44

Source documentation

Lie homomorphisms preserve the finite Dynkin polynomial.

theorem finiteDynkinPolynomial_map {L' : Type*} [LieRing L'] [LieAlgebra ℝ L']
    (f : L →ₗ⁅ℝ⁆ L') {c n : ℕ} (coeff : DynkinCoefficients c n) (X : Fin n → L) :
    f (finiteDynkinPolynomial coeff X) = finiteDynkinPolynomial coeff (fun i => f (X i)) := by
…

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

theorem OAI.PolycyclicRecognition.norm_finiteDynkinPolynomial_le line 51

Source documentation

All coefficient counting and bracket estimates are proved here; only the identity identifying this polynomial with the group product is external.

theorem norm_finiteDynkinPolynomial_le (b : Basis J ℝ L) {c n : ℕ}
    (coeff : DynkinCoefficients c n) (hcoeff : ∀ d w, |coeff d w| ≤ (2 : ℝ) ^ c)
    (X : Fin n → L) {C M : ℝ} (hC : 0 ≤ C) (hM : 0 ≤ M)
    (hbracket : ∀ i j l, |b.repr ⁅b i, b j⁆ l| ≤ C)
    (hX : ∀ i, ‖b.equivFun (X i)‖ ≤ M) :
    ‖b.equivFun (finiteDynkinPolynomial coeff X)‖ ≤
      (c : ℝ) * 2 ^ c * (1 + (Fintype.card J : ℝ) ^ 2 * C) ^ c *
        (1 + M) ^ c * (1 + (n : ℝ)) ^ c := by
…

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