OAI/GroupTheory/PolycyclicRecognition/Algebra/HomogeneousUniversalLogarithm.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.IsHomogeneousRationalWord.zero line 13
2. theorem OAI.PolycyclicRecognition.IsHomogeneousRationalWord.add line 17
3. theorem OAI.PolycyclicRecognition.IsHomogeneousRationalWord.smul line 26
4. theorem OAI.PolycyclicRecognition.homogeneousRationalWord_single line 33
5. theorem OAI.PolycyclicRecognition.weightedWord_coefficient_homogeneous line 43
6. theorem OAI.PolycyclicRecognition.weightedWordSpan_coefficient_homogeneous line 57
7. theorem OAI.PolycyclicRecognition.universalLogarithmCoefficient_homogeneous line 68
8. theorem OAI.PolycyclicRecognition.universalLogarithmCoefficient_lie_expansion line 75

   Source documentation

   Each positive-degree universal logarithm coefficient is a finite Lie polynomial.

   theorem universalLogarithmCoefficient_lie_expansion {A : Type*} [Ring A] [Algebra ℚ A]
       (c n d : ℕ) (X : Fin n → A) :
       rationalWordEvaluation X (universalLogarithmCoefficient c n (d + 1)) =
         ∑ w : Fin (d + 1) → Fin n,
           ((d + 1 : ℚ)⁻¹ * (universalLogarithmCoefficient c n (d + 1)).coeff (wordOfFn w)) •
             evalBracketWord X (rightNestedWord d w) :=
   …

   Mentions: OAI.PolycyclicRecognition.rationalWordEvaluation, OAI.PolycyclicRecognition.universalLogarithmCoefficient, OAI.PolycyclicRecognition.wordOfFn, OAI.PolycyclicRecognition.evalBracketWord, OAI.PolycyclicRecognition.rightNestedWord