FiniteLieSmooth.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Smoothness of finite Lie polynomials

A finite-dimensional Lie bracket is a continuous bilinear map in basis coordinates. Consequently the actual finite Dynkin expressions are smooth; no smoothness of a chosen logarithm chart is assumed here.

def OAI.PolycyclicRecognition.finiteLieBracket line 29
Source documentation
Continuous bilinear realization of the given finite-dimensional bracket.
```
def finiteLieBracket : L →L[ℝ] L →L[ℝ] L :=
…
```
theorem OAI.PolycyclicRecognition.finiteLieBracket_apply line 35
theorem OAI.PolycyclicRecognition.contDiff_evalBracketWord line 41
Source documentation
Any fixed evaluated bracket word in smooth input functions is smooth.
```
theorem contDiff_evalBracketWord (X : V → I → L)
    (hX : ∀ i, ContDiff ℝ n (fun v => X v i)) (w : FreeMagma I) :
    ContDiff ℝ n (fun v => evalBracketWord (X v) w) := by
…
```
Mentions: OAI.PolycyclicRecognition.evalBracketWord
theorem OAI.PolycyclicRecognition.contDiff_finiteDynkinPolynomial line 50
Source documentation
The finite published Dynkin expression is smooth in all its logarithms.
```
theorem contDiff_finiteDynkinPolynomial {c k : ℕ} (coeff : DynkinCoefficients c k)
    (X : V → Fin k → L) (hX : ∀ i, ContDiff ℝ n (fun v => X v i)) :
    ContDiff ℝ n (fun v => finiteDynkinPolynomial coeff (X v)) := by
…
```
Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial