ParametricLieWords.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Lie words as functions of their structure constants

The bilinear bracket itself varies in a finite-dimensional vector space. Word evaluation is smooth jointly in that bracket and the input vectors, so word identities and normalization equations persist under limits.

theorem OAI.PolycyclicRecognition.norm_bilinear_le_of_bound line 24

Source documentation

A bound on bilinear evaluations bounds the iterated operator norm.

theorem norm_bilinear_le_of_bound (B : V →L[ℝ] V →L[ℝ] V) {C : ℝ}
    (hC : 0 ≤ C) (h : ∀ x y, ‖B x y‖ ≤ C * ‖x‖ * ‖y‖) : ‖B‖ ≤ C := by
…

def OAI.PolycyclicRecognition.evalBilinearWord line 32

Source documentation

Evaluate a bracket word with a specified continuous bilinear bracket.

def evalBilinearWord (B : V →L[ℝ] V →L[ℝ] V) (X : I → V) : FreeMagma I → V
  | .of i => X i
  | .mul a b => B (evalBilinearWord B X a) (evalBilinearWord B X b)

variable {P : Type*} [NormedAddCommGroup P] [NormedSpace ℝ P]
  {n : ℕ∞}

/-- Smooth dependence of a finite word on both bracket and generator data. -/

theorem OAI.PolycyclicRecognition.contDiff_evalBilinearWord line 40

Source documentation

Smooth dependence of a finite word on both bracket and generator data.

theorem contDiff_evalBilinearWord (B : P → V →L[ℝ] V →L[ℝ] V)
    (X : P → I → V) (hB : ContDiff ℝ n B)
    (hX : ∀ i, ContDiff ℝ n (fun p => X p i)) (w : FreeMagma I) :
    ContDiff ℝ n (fun p => evalBilinearWord (B p) (X p) w) := by
…

Mentions: OAI.PolycyclicRecognition.evalBilinearWord

def OAI.PolycyclicRecognition.IsLieBracket line 50
Source documentation
The defining identities of a real Lie bracket, with bilinearity supplied by its continuous-linear-map type.
```
def IsLieBracket (B : V →L[ℝ] V →L[ℝ] V) : Prop :=
…
```
theorem OAI.PolycyclicRecognition.isClosed_setOf_isLieBracket line 54
Source documentation
Alternation and Jacobi are closed conditions on the bracket.
```
theorem isClosed_setOf_isLieBracket :
    IsClosed {B : V →L[ℝ] V →L[ℝ] V | IsLieBracket B} := by
…
```
Mentions: OAI.PolycyclicRecognition.IsLieBracket
theorem OAI.PolycyclicRecognition.isClosed_bilinearWord_eq line 71
Source documentation
A fixed word equation is closed even while both bracket and generators vary. This is the normalization condition used by rescaled word bases.
```
theorem isClosed_bilinearWord_eq [Fintype I] (w : FreeMagma I) (v : V) :
    IsClosed {p : (V →L[ℝ] V →L[ℝ] V) × (I → V) |
      evalBilinearWord p.1 p.2 w = v} := by
…
```
Mentions: OAI.PolycyclicRecognition.evalBilinearWord

theorem OAI.PolycyclicRecognition.isClosed_wordNormalizations line 81

Source documentation

All finite word-normalization equations hold on a closed parameter set.

theorem isClosed_wordNormalizations [Fintype I] {J : Type*}
    (w : J → FreeMagma I) (v : J → V) :
    IsClosed {p : (V →L[ℝ] V →L[ℝ] V) × (I → V) |
      ∀ j, evalBilinearWord p.1 p.2 (w j) = v j} := by
…

Mentions: OAI.PolycyclicRecognition.evalBilinearWord