OAI/GroupTheory/PolycyclicRecognition/Geometry/LieWordDerivative.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual derivatives of finite Lie polynomials

The finite-dimensional bracket is continuous in the given norm. The resulting differential is the algebraic word differential.

  1. def OAI.PolycyclicRecognition.normedLieBracket line 21

    Source documentation

    Continuous realization of the bracket in the given finite-dimensional norm.

    def normedLieBracket : L →L[ℝ] L →L[ℝ] L :=
…
  2. theorem OAI.PolycyclicRecognition.hasFDerivAt_evalBracketWord line 27
  3. theorem OAI.PolycyclicRecognition.hasFDerivAt_finiteDynkinPolynomial line 45