OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialGrowthLinearImage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

An infinite real linear image of an infinite polynomial-growth group

This is the linear-representation conclusion in Kleiner, JAMS 23 (2010), Sections 4 and 5. Both the harmonic finite-dimensionality and the nonconstant harmonic-function construction are proved here, rather than assumed.

  1. theorem OAI.PolycyclicRecognition.infinite_generating_finset_nonempty line 16
  2. theorem OAI.PolycyclicRecognition.polynomial_growth_infinite_real_linear_image line 24