LieWordDifference.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Finite differences of Lie words along the lower central series

The nonlinear part of a bracket polynomial raises the filtration also for finite differences, not just infinitesimal ones. This supports the explicit inverse of a BCH translation.

theorem OAI.PolycyclicRecognition.lie_sub_lie_decomposition line 20
theorem OAI.PolycyclicRecognition.evalBracketWord_sub_mem line 25
theorem OAI.PolycyclicRecognition.evalBracketWord_mul_sub_mem_succ line 34
def OAI.PolycyclicRecognition.wordLinearPart line 54
Source documentation
The degree-one part of a word as a linear map in its input letters.
```
def wordLinearPart : FreeMagma I → (I → L) →ₗ[ℝ] L
  | .of i => LinearMap.proj i
  | .mul _ _ => 0
```
def OAI.PolycyclicRecognition.finiteDynkinLinearPart line 58
theorem OAI.PolycyclicRecognition.evalBracketWord_sub_linear_mem_succ line 63
theorem OAI.PolycyclicRecognition.finiteDynkinPolynomial_sub_linear_mem_succ line 75