1. FormalConjectures
  2. Wikipedia
  3. GromovPolynomialGrowth
/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Gromov's theorem on groups of polynomial growth

Reference:

/- Note: this was obtained in work with Kasia Jankiewicz and Catherine Pfaff, and using Claude 4.0 Sonnet: https://claude.ai/share/918bb269-bd28-4c09-b84e-cab579c836e8 -/ namespace GromovPolynomialGrowth open Filter variable {G : Type*} [Group G]

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.

@[category test, AMS 20] 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 := G:Type u_1inst✝¹:Group Ginst✝:Infinite GS:Set GhS:S.Finiteh:Subgroup.closure S = ⊤C:ℝd:ℕ⊢ ∃ n, C * ↑n ^ d < ↑(GrowthFunction S n) G:Type u_1inst✝¹:Group Ginst✝:Infinite GS:Set GhS:S.Finiteh:Subgroup.closure S = ⊤C:ℝd:ℕhd:d = 0⊢ ∃ n, C * ↑n ^ d < ↑(GrowthFunction S n)G:Type u_1inst✝¹:Group Ginst✝:Infinite GS:Set GhS:S.Finiteh:Subgroup.closure S = ⊤C:ℝd:ℕhd:¬d = 0⊢ ∃ n, C * ↑n ^ d < ↑(GrowthFunction S n) G:Type u_1inst✝¹:Group Ginst✝:Infinite GS:Set GhS:S.Finiteh:Subgroup.closure S = ⊤C:ℝd:ℕhd:d = 0⊢ ∃ n, C * ↑n ^ d < ↑(GrowthFunction S n) G:Type u_1inst✝¹:Group Ginst✝:Infinite GS:Set GhS:S.Finiteh:Subgroup.closure S = ⊤C:ℝd:ℕhd:d = 0n:ℕleft✝:n ≥ 0hn:⌈C⌉₊ < GrowthFunction S n⊢ ∃ n, C * ↑n ^ d < ↑(GrowthFunction S n) G:Type u_1inst✝¹:Group Ginst✝:Infinite GS:Set GhS:S.Finiteh:Subgroup.closure S = ⊤C:ℝd:ℕhd:d = 0n:ℕleft✝:n ≥ 0hn:⌈C⌉₊ < GrowthFunction S n⊢ C * ↑n ^ d < ↑(GrowthFunction S n) grw [Nat.le_ceil CG:Type u_1inst✝¹:Group Ginst✝:Infinite GS:Set GhS:S.Finiteh:Subgroup.closure S = ⊤C:ℝd:ℕhd:d = 0n:ℕleft✝:n ≥ 0hn:⌈C⌉₊ < GrowthFunction S n⊢ ↑⌈C⌉₊ * ↑n ^ d < ↑(GrowthFunction S n) All goals completed! 🐙 G:Type u_1inst✝¹:Group Ginst✝:Infinite GS:Set GhS:S.Finiteh:Subgroup.closure S = ⊤C:ℝd:ℕhd:¬d = 0⊢ ∃ n, C * ↑n ^ d < ↑(GrowthFunction S n) exact ⟨0, G:Type u_1inst✝¹:Group Ginst✝:Infinite GS:Set GhS:S.Finiteh:Subgroup.closure S = ⊤C:ℝd:ℕhd:¬d = 0⊢ C * ↑0 ^ d < ↑(GrowthFunction S 0) All goals completed! 🐙⟩ variable (G)

Gromov's Polynomial Growth Theorem : A finitely generated group has polynomial growth if and only if it is virtually nilpotent.

@[category research solved, AMS 20] theorem declaration uses 'sorry'GromovPolynomialGrowthTheorem [Group.FG G] : HasPolynomialGrowth G ↔ Group.IsVirtuallyNilpotent G := G:Type u_1inst✝¹:Group Ginst✝:Group.FG G⊢ HasPolynomialGrowth G ↔ Group.IsVirtuallyNilpotent G All goals completed! 🐙 end GromovPolynomialGrowth