theorem
GromovPolynomialGrowth.growthFunction_not_polynomial_of_infinite
{G : Type u_1}
[Group G]
[Infinite G]
{S : Set G}
(hS : S.Finite)
(h : Subgroup.closure S = ⊤)
{C : ℝ}
(d : ℕ)
:
∃ (n : ℕ), C * ↑n ^ d < ↑(GrowthFunction S n)
Infinite groups do not satisfy polynomial growth over ℕ for any degree d because when
d = 0 this reduces to the unbounded nature of growthFunction while n = 0 works when d ≠ 0.
Thus a finitely-generated infinite nilpotent group would be a counter-example to
Gromov's theorem when quantifying over all of ℕ, and so n = 0 should be excluded.
theorem
GromovPolynomialGrowth.GromovPolynomialGrowthTheorem
(G : Type u_1)
[Group G]
[Group.FG G]
:
Gromov's Polynomial Growth Theorem : A finitely generated group has polynomial growth if and only if it is virtually nilpotent.