FiniteLieNorm.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Bracket bounds from finitely many structure constants

The norm is the coordinate maximum in a specified basis. Consequently the bound applies uniformly to every rescaled word basis from the box calculus.

theorem OAI.PolycyclicRecognition.basis_bracket_coordinate line 24
Source documentation
The bracket in coordinates is the bilinear expression in the actual structure constants.
```
theorem basis_bracket_coordinate (x y : L) (l : J) :
    b.repr ⁅x, y⁆ l = ∑ i, ∑ j, b.repr x i * b.repr y j * b.repr ⁅b i, b j⁆ l := by
…
```

theorem OAI.PolycyclicRecognition.norm_basis_bracket_le line 32

Source documentation

Bounding the finitely many basis brackets bounds the full bracket as a bilinear map, in the coordinate maximum norm.

theorem norm_basis_bracket_le {C : ℝ} (hC : 0 ≤ C)
    (hbracket : ∀ i j l, |b.repr ⁅b i, b j⁆ l| ≤ C) (x y : L) :
    ‖b.equivFun ⁅x, y⁆‖ ≤
      ((Fintype.card J : ℝ) ^ 2 * C) * ‖b.equivFun x‖ * ‖b.equivFun y‖ := by
…

def OAI.PolycyclicRecognition.bracketWordLength line 57

Source documentation

Number of input letters in a bracket word.

def bracketWordLength {I : Type*} : FreeMagma I → ℕ
  | .of _ => 1
  | .mul u v => bracketWordLength u + bracketWordLength v

/-- Number of bracket operations in the word. -/

def OAI.PolycyclicRecognition.bracketWordNodes line 62

Source documentation

Number of bracket operations in the word.

def bracketWordNodes {I : Type*} : FreeMagma I → ℕ
  | .of _ => 0
  | .mul u v => bracketWordNodes u + bracketWordNodes v + 1

theorem OAI.PolycyclicRecognition.bracketWordLength_eq_nodes_add_one line 66

theorem OAI.PolycyclicRecognition.norm_basis_evalBracketWord_le line 74

Source documentation

Evaluation of each Lie word is bounded by the number of its brackets and letters. This is uniform over a family with bounded structure constants.

theorem norm_basis_evalBracketWord_le {I : Type*} (X : I → 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) (w : FreeMagma I) :
    ‖b.equivFun (evalBracketWord X w)‖ ≤
      ((Fintype.card J : ℝ) ^ 2 * C) ^ bracketWordNodes w * M ^ bracketWordLength w := by
…

Mentions: OAI.PolycyclicRecognition.evalBracketWord, OAI.PolycyclicRecognition.bracketWordNodes, OAI.PolycyclicRecognition.bracketWordLength

theorem OAI.PolycyclicRecognition.norm_basis_liePolynomial_le line 96

Source documentation

The corresponding bound for an actual finite Lie polynomial.

theorem norm_basis_liePolynomial_le {I A : Type*} [Fintype A]
    (X : I → L) (words : A → FreeMagma I) (coeff : A → ℝ)
    {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 (∑ a, coeff a • evalBracketWord X (words a))‖ ≤
      ∑ a, |coeff a| * (((Fintype.card J : ℝ) ^ 2 * C) ^ bracketWordNodes (words a) *
        M ^ bracketWordLength (words a)) := by
…

Mentions: OAI.PolycyclicRecognition.evalBracketWord, OAI.PolycyclicRecognition.bracketWordNodes, OAI.PolycyclicRecognition.bracketWordLength