OAI/GroupTheory/PolycyclicRecognition/Analysis/PolynomialHarmonicFiniteDimensional.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-dimensionality of polynomial-growth harmonic functions

This proves the discrete Cayley-graph form of Kleiner, Theorem 1.4, using the Poincare, good-scale, spectral and averaging arguments.

  1. theorem OAI.PolycyclicRecognition.polynomialHarmonicFunctions_finite line 16
  2. theorem OAI.PolycyclicRecognition.polynomialHarmonicFunctions_finite_of_word_growth line 57