OAI/GroupTheory/PolycyclicRecognition/Analysis/PolynomialHarmonicFunctions.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The translation representation on polynomial-growth harmonic functions

  1. def OAI.PolycyclicRecognition.PolynomiallyBoundedOnWords line 11
  2. def OAI.PolycyclicRecognition.polynomialWordFunctions line 14
  3. def OAI.PolycyclicRecognition.cayleyHarmonicFunctions line 28
  4. def OAI.PolycyclicRecognition.polynomialHarmonicFunctions line 40
  5. def OAI.PolycyclicRecognition.cayleyLeftTranslate line 43
  6. theorem OAI.PolycyclicRecognition.cayleyHarmonic_leftTranslate line 46
  7. theorem OAI.PolycyclicRecognition.polynomialWord_leftTranslate line 51
  8. def OAI.PolycyclicRecognition.polynomialHarmonicLeftTranslation line 67
  9. def OAI.PolycyclicRecognition.polynomialHarmonicRepresentation line 81