Wikipedia · test · AMS 20
easyknown result, no worker yet
Gromov's theorem on groups of polynomial growth
Exercise · growthFunction_not_polynomial_of_infinite
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.
Formal statement · Lean 4.lean
theorem growthFunction_not_polynomial_of_infinite [Infinite G] {S : Set G} (hS : S.Finite)
(h : Subgroup.closure S = ⊤) {C : ℝ} (d : ℕ) :
∃ (n : ℕ), C * n ^ d < GrowthFunction S n := by
sorryProof. sorry
Nobody has tried yet.