/-
Copyright 2026 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.
-/
module
public import FormalConjecturesForMathlib.Order.Filter.atTopBot.Finset
public import Mathlib.Data.Fin.VecNotation
public import Mathlib.Data.Real.Basic
public import Mathlib.Data.Set.Card
public import Mathlib.GroupTheory.Finiteness
public import Mathlib.Tactic.SetNotationForOrder
import Mathlib.Tactic@[expose] public sectionopen Filternamespace GromovPolynomialGrowthvariable {G : Type*} [Group G]
The CayleyBall is the ball of radius n in the Cayley graph of a group G with generating
set S.
def CayleyBall (S : Set G) (n : ℕ) : Set G :=
{g : G | ∃ (l : List G), l.length ≤ n ∧ (∀ s ∈ l, s ∈ S ∨ s⁻¹ ∈ S) ∧ l.prod = g}theorem cayleyBall_zero (S : Set G) :
CayleyBall S 0 = {1} := G:Type u_1inst✝:Group GS:Set G⊢ CayleyBall S 0 = {1}
All goals completed! 🐙G:Type u_1inst✝:Group GS:Set GhS:S.Finiten:ℕhu:(S ∪ (fun x ↦ x)⁻¹ '' S).Finitehf:∀ (m : ℕ), {f | ∀ (i : Fin m), f i ∈ S ∨ (f i)⁻¹ ∈ S}.Finitethis:{l | l.length ≤ n ∧ ∀ s ∈ l, s ∈ S ∨ s⁻¹ ∈ S}.Finite⊢ (CayleyBall S n).Finite
exact (this.image List.prod).subset fun _ _ ↦ G:Type u_1inst✝:Group GS:Set GhS:S.Finiten:ℕhu:(S ∪ (fun x ↦ x)⁻¹ '' S).Finitehf:∀ (m : ℕ), {f | ∀ (i : Fin m), f i ∈ S ∨ (f i)⁻¹ ∈ S}.Finitethis:{l | l.length ≤ n ∧ ∀ s ∈ l, s ∈ S ∨ s⁻¹ ∈ S}.Finitex✝¹:Gx✝:x✝¹ ∈ CayleyBall S n⊢ x✝¹ ∈ List.prod '' {l | l.length ≤ n ∧ ∀ s ∈ l, s ∈ S ∨ s⁻¹ ∈ S} All goals completed! 🐙
The GrowthFunction of a group G with respect to a set S counts the number of group
elements that can be reached by words of length at most n in S.
noncomputable def GrowthFunction (S : Set G) (n : ℕ) : ℕ :=
(CayleyBall S n).ncardtheorem growthFunction_zero (S : Set G) :
GrowthFunction S 0 = 1 := G:Type u_1inst✝:Group GS:Set G⊢ GrowthFunction S 0 = 1
All goals completed! 🐙The identity is always in the Cayley ball.
lemma one_mem_cayleyBall (S : Set G) (n : ℕ) :
1 ∈ CayleyBall S n := G:Type u_1inst✝:Group GS:Set Gn:ℕ⊢ 1 ∈ CayleyBall S n
G:Type u_1inst✝:Group GS:Set Gn:ℕ⊢ ∃ l, l.length ≤ n ∧ (∀ s ∈ l, s ∈ S ∨ s⁻¹ ∈ S) ∧ l.prod = 1
G:Type u_1inst✝:Group GS:Set Gn:ℕ⊢ ∅.length ≤ n ∧ (∀ s ∈ ∅, s ∈ S ∨ s⁻¹ ∈ S) ∧ ∅.prod = 1
All goals completed! 🐙The Cayley ball is monotonic in its radius.
lemma cayleyBall_monotone (S : Set G) {m n : ℕ} (h : m ≤ n) :
CayleyBall S m ⊆ CayleyBall S n := G:Type u_1inst✝:Group GS:Set Gm:ℕn:ℕh:m ≤ n⊢ CayleyBall S m ⊆ CayleyBall S n
G:Type u_1inst✝:Group GS:Set Gm:ℕn:ℕh:m ≤ n⊢ ∀ (a : G) (x : List G),
x.length ≤ m → (∀ s ∈ x, s ∈ S ∨ s⁻¹ ∈ S) → x.prod = a → ∃ l, l.length ≤ n ∧ (∀ s ∈ l, s ∈ S ∨ s⁻¹ ∈ S) ∧ l.prod = a
exact fun g l lLength LSubS lProdG ↦ ⟨l, G:Type u_1inst✝:Group GS:Set Gm:ℕn:ℕh:m ≤ ng:Gl:List GlLength:l.length ≤ mLSubS:∀ s ∈ l, s ∈ S ∨ s⁻¹ ∈ SlProdG:l.prod = g⊢ l.length ≤ n All goals completed! 🐙, LSubS, lProdG⟩
Closure property: if g ∈ CayleyBall S m and h ∈ CayleyBall S n, then
g * h ∈ CayleyBall S (m + n).
lemma cayleyBall_mul (S : Set G) {g h : G} {m n : ℕ}
(hg : g ∈ CayleyBall S m) (hh : h ∈ CayleyBall S n) :
g * h ∈ CayleyBall S (m + n) := G:Type u_1inst✝:Group GS:Set Gg:Gh:Gm:ℕn:ℕhg:g ∈ CayleyBall S mhh:h ∈ CayleyBall S n⊢ g * h ∈ CayleyBall S (m + n)
G:Type u_1inst✝:Group GS:Set Gg:Gh:Gm:ℕn:ℕhg:∃ l, l.length ≤ m ∧ (∀ s ∈ l, s ∈ S ∨ s⁻¹ ∈ S) ∧ l.prod = ghh:∃ l, l.length ≤ n ∧ (∀ s ∈ l, s ∈ S ∨ s⁻¹ ∈ S) ∧ l.prod = h⊢ ∃ l, l.length ≤ m + n ∧ (∀ s ∈ l, s ∈ S ∨ s⁻¹ ∈ S) ∧ l.prod = g * h
G:Type u_1inst✝:Group GS:Set Gg:Gh:Gm:ℕn:ℕhh:∃ l, l.length ≤ n ∧ (∀ s ∈ l, s ∈ S ∨ s⁻¹ ∈ S) ∧ l.prod = hlg:List GlgLength:lg.length ≤ mlgSubS:∀ s ∈ lg, s ∈ S ∨ s⁻¹ ∈ SlgProd:lg.prod = g⊢ ∃ l, l.length ≤ m + n ∧ (∀ s ∈ l, s ∈ S ∨ s⁻¹ ∈ S) ∧ l.prod = g * h
G:Type u_1inst✝:Group GS:Set Gg:Gh:Gm:ℕn:ℕlg:List GlgLength:lg.length ≤ mlgSubS:∀ s ∈ lg, s ∈ S ∨ s⁻¹ ∈ SlgProd:lg.prod = glh:List GlhLength:lh.length ≤ nlhSubS:∀ s ∈ lh, s ∈ S ∨ s⁻¹ ∈ SlhProd:lh.prod = h⊢ ∃ l, l.length ≤ m + n ∧ (∀ s ∈ l, s ∈ S ∨ s⁻¹ ∈ S) ∧ l.prod = g * h
refine ⟨lg ++ lh, ?_, ?_, G:Type u_1inst✝:Group GS:Set Gg:Gh:Gm:ℕn:ℕlg:List GlgLength:lg.length ≤ mlgSubS:∀ s ∈ lg, s ∈ S ∨ s⁻¹ ∈ SlgProd:lg.prod = glh:List GlhLength:lh.length ≤ nlhSubS:∀ s ∈ lh, s ∈ S ∨ s⁻¹ ∈ SlhProd:lh.prod = h⊢ (lg ++ lh).prod = g * h All goals completed! 🐙⟩
G:Type u_1inst✝:Group GS:Set Gg:Gh:Gm:ℕn:ℕlg:List GlgLength:lg.length ≤ mlgSubS:∀ s ∈ lg, s ∈ S ∨ s⁻¹ ∈ SlgProd:lg.prod = glh:List GlhLength:lh.length ≤ nlhSubS:∀ s ∈ lh, s ∈ S ∨ s⁻¹ ∈ SlhProd:lh.prod = h⊢ (lg ++ lh).length ≤ m + n G:Type u_1inst✝:Group GS:Set Gg:Gh:Gm:ℕn:ℕlg:List GlgLength:lg.length ≤ mlgSubS:∀ s ∈ lg, s ∈ S ∨ s⁻¹ ∈ SlgProd:lg.prod = glh:List GlhLength:lh.length ≤ nlhSubS:∀ s ∈ lh, s ∈ S ∨ s⁻¹ ∈ SlhProd:lh.prod = h⊢ lg.length + lh.length ≤ m + n
All goals completed! 🐙
G:Type u_1inst✝:Group GS:Set Gg:Gh:Gm:ℕn:ℕlg:List GlgLength:lg.length ≤ mlgSubS:∀ s ∈ lg, s ∈ S ∨ s⁻¹ ∈ SlgProd:lg.prod = glh:List GlhLength:lh.length ≤ nlhSubS:∀ s ∈ lh, s ∈ S ∨ s⁻¹ ∈ SlhProd:lh.prod = h⊢ ∀ s ∈ lg ++ lh, s ∈ S ∨ s⁻¹ ∈ S G:Type u_1inst✝:Group GS:Set Gg:Gh:Gm:ℕn:ℕlg:List GlgLength:lg.length ≤ mlgSubS:∀ s ∈ lg, s ∈ S ∨ s⁻¹ ∈ SlgProd:lg.prod = glh:List GlhLength:lh.length ≤ nlhSubS:∀ s ∈ lh, s ∈ S ∨ s⁻¹ ∈ SlhProd:lh.prod = hs:GsIn:s ∈ lg ++ lh⊢ s ∈ S ∨ s⁻¹ ∈ S
G:Type u_1inst✝:Group GS:Set Gg:Gh:Gm:ℕn:ℕlg:List GlgLength:lg.length ≤ mlgSubS:∀ s ∈ lg, s ∈ S ∨ s⁻¹ ∈ SlgProd:lg.prod = glh:List GlhLength:lh.length ≤ nlhSubS:∀ s ∈ lh, s ∈ S ∨ s⁻¹ ∈ SlhProd:lh.prod = hs:GsIn:s ∈ lg ∨ s ∈ lh⊢ s ∈ S ∨ s⁻¹ ∈ S
cases sIn with
G:Type u_1inst✝:Group GS:Set Gg:Gh✝:Gm:ℕn:ℕlg:List GlgLength:lg.length ≤ mlgSubS:∀ s ∈ lg, s ∈ S ∨ s⁻¹ ∈ SlgProd:lg.prod = glh:List GlhLength:lh.length ≤ nlhSubS:∀ s ∈ lh, s ∈ S ∨ s⁻¹ ∈ SlhProd:lh.prod = hs:Gh:s ∈ lg⊢ s ∈ S ∨ s⁻¹ ∈ S All goals completed! 🐙
G:Type u_1inst✝:Group GS:Set Gg:Gh✝:Gm:ℕn:ℕlg:List GlgLength:lg.length ≤ mlgSubS:∀ s ∈ lg, s ∈ S ∨ s⁻¹ ∈ SlgProd:lg.prod = glh:List GlhLength:lh.length ≤ nlhSubS:∀ s ∈ lh, s ∈ S ∨ s⁻¹ ∈ SlhProd:lh.prod = hs:Gh:s ∈ lh⊢ s ∈ S ∨ s⁻¹ ∈ S All goals completed! 🐙
If g ∈ CayleyBall S n, then g⁻¹ ∈ CayleyBall S n.
lemma cayleyBall_inv (S : Set G) {g : G} {n : ℕ}
(hg : g ∈ CayleyBall S n) :
g⁻¹ ∈ CayleyBall S n := G:Type u_1inst✝:Group GS:Set Gg:Gn:ℕhg:g ∈ CayleyBall S n⊢ g⁻¹ ∈ CayleyBall S n
G:Type u_1inst✝:Group GS:Set Gg:Gn:ℕhg:∃ l, l.length ≤ n ∧ (∀ s ∈ l, s ∈ S ∨ s⁻¹ ∈ S) ∧ l.prod = g⊢ ∃ l, l.length ≤ n ∧ (∀ s ∈ l, s ∈ S ∨ s⁻¹ ∈ S) ∧ l.prod = g⁻¹
G:Type u_1inst✝:Group GS:Set Gg:Gn:ℕlg:List GlgLength:lg.length ≤ nlgSubS:∀ s ∈ lg, s ∈ S ∨ s⁻¹ ∈ SlgProd:lg.prod = g⊢ ∃ l, l.length ≤ n ∧ (∀ s ∈ l, s ∈ S ∨ s⁻¹ ∈ S) ∧ l.prod = g⁻¹
refine ⟨lg.reverse.map (·⁻¹), G:Type u_1inst✝:Group GS:Set Gg:Gn:ℕlg:List GlgLength:lg.length ≤ nlgSubS:∀ s ∈ lg, s ∈ S ∨ s⁻¹ ∈ SlgProd:lg.prod = g⊢ (List.map (fun x ↦ x⁻¹) lg.reverse).length ≤ n All goals completed! 🐙, ?_,
G:Type u_1inst✝:Group GS:Set Gg:Gn:ℕlg:List GlgLength:lg.length ≤ nlgSubS:∀ s ∈ lg, s ∈ S ∨ s⁻¹ ∈ SlgProd:lg.prod = g⊢ (List.map (fun x ↦ x⁻¹) lg.reverse).prod = g⁻¹ All goals completed! 🐙⟩
G:Type u_1inst✝:Group GS:Set Gg:Gn:ℕlg:List GlgLength:lg.length ≤ nlgSubS:∀ s ∈ lg, s ∈ S ∨ s⁻¹ ∈ SlgProd:lg.prod = gs:GsIn:s ∈ List.map (fun x ↦ x⁻¹) lg.reverse⊢ s ∈ S ∨ s⁻¹ ∈ S
G:Type u_1inst✝:Group GS:Set Gg:Gn:ℕlg:List GlgLength:lg.length ≤ nlgSubS:∀ s ∈ lg, s ∈ S ∨ s⁻¹ ∈ SlgProd:lg.prod = gs:GsIn:s⁻¹ ∈ lg⊢ s ∈ S ∨ s⁻¹ ∈ S
G:Type u_1inst✝:Group GS:Set Gg:Gn:ℕlg:List GlgLength:lg.length ≤ nlgSubS:∀ s ∈ lg, s ∈ S ∨ s⁻¹ ∈ SlgProd:lg.prod = gs:GsIn:s⁻¹ ∈ lgthis:s⁻¹ ∈ S ∨ s⁻¹⁻¹ ∈ S⊢ s ∈ S ∨ s⁻¹ ∈ S
G:Type u_1inst✝:Group GS:Set Gg:Gn:ℕlg:List GlgLength:lg.length ≤ nlgSubS:∀ s ∈ lg, s ∈ S ∨ s⁻¹ ∈ SlgProd:lg.prod = gs:GsIn:s⁻¹ ∈ lgthis:s⁻¹ ∈ S ∨ s ∈ S⊢ s ∈ S ∨ s⁻¹ ∈ S
All goals completed! 🐙lemma mem_cayleyBall_one_of_mem {S : Set G} {g : G} (hg : g ∈ S) : g ∈ CayleyBall S 1 :=
⟨[g], G:Type u_1inst✝:Group GS:Set Gg:Ghg:g ∈ S⊢ [g].length ≤ 1 ∧ (∀ s ∈ [g], s ∈ S ∨ s⁻¹ ∈ S) ∧ [g].prod = g All goals completed! 🐙⟩lemma exists_cayleyBall_mem_of_closure_eq_top {S : Set G} (h : Subgroup.closure S = ⊤) (g : G) :
∃ n, g ∈ CayleyBall S n := G:Type u_1inst✝:Group GS:Set Gh:Subgroup.closure S = ⊤g:G⊢ ∃ n, g ∈ CayleyBall S n
induction h ▸ Subgroup.mem_top g using Subgroup.closure_induction with
G:Type u_1inst✝:Group GS:Set Gh:Subgroup.closure S = ⊤g:Gx✝:Ghx✝:x✝ ∈ S⊢ ∃ n, x✝ ∈ CayleyBall S n All goals completed! 🐙
G:Type u_1inst✝:Group GS:Set Gh:Subgroup.closure S = ⊤g:G⊢ ∃ n, 1 ∈ CayleyBall S n All goals completed! 🐙
G:Type u_1inst✝:Group GS:Set Gh:Subgroup.closure S = ⊤g:Gx✝:Gy✝:Ghx✝:x✝ ∈ Subgroup.closure Shy✝:y✝ ∈ Subgroup.closure Shg₁:∃ n, x✝ ∈ CayleyBall S nhg₂:∃ n, y✝ ∈ CayleyBall S n⊢ ∃ n, x✝ * y✝ ∈ CayleyBall S n
G:Type u_1inst✝:Group GS:Set Gh:Subgroup.closure S = ⊤g:Gx✝:Gy✝:Ghx✝:x✝ ∈ Subgroup.closure Shy✝:y✝ ∈ Subgroup.closure Shg₂:∃ n, y✝ ∈ CayleyBall S nn₁:ℕhn₁:x✝ ∈ CayleyBall S n₁⊢ ∃ n, x✝ * y✝ ∈ CayleyBall S n
G:Type u_1inst✝:Group GS:Set Gh:Subgroup.closure S = ⊤g:Gx✝:Gy✝:Ghx✝:x✝ ∈ Subgroup.closure Shy✝:y✝ ∈ Subgroup.closure Sn₁:ℕhn₁:x✝ ∈ CayleyBall S n₁n₂:ℕhn₂:y✝ ∈ CayleyBall S n₂⊢ ∃ n, x✝ * y✝ ∈ CayleyBall S n
All goals completed! 🐙
G:Type u_1inst✝:Group GS:Set Gh:Subgroup.closure S = ⊤g:Gx✝:Ghx✝:x✝ ∈ Subgroup.closure Shg:∃ n, x✝ ∈ CayleyBall S n⊢ ∃ n, x✝⁻¹ ∈ CayleyBall S n
G:Type u_1inst✝:Group GS:Set Gh:Subgroup.closure S = ⊤g:Gx✝:Ghx✝:x✝ ∈ Subgroup.closure Sn:ℕhn:x✝ ∈ CayleyBall S n⊢ ∃ n, x✝⁻¹ ∈ CayleyBall S n
All goals completed! 🐙In an infinite group, the growth function with respect to a finite generating set is unbounded.
G:Type u_1inst✝¹:Group Ginst✝:Infinite GS:Set GhS:S.Finiteh:Subgroup.closure S = ⊤this:(n : ℕ) → Fintype ↑(CayleyBall S n)A:Finset GhA:A.Nonemptyn:↥A → ℕhn:∀ (a : ↥A), ↑a ∈ CayleyBall S (n a)N:ℕ := (Set.range n).toFinset.max' ⋯⊢ ∃ a, A ⊆ (CayleyBall S a).toFinset
G:Type u_1inst✝¹:Group Ginst✝:Infinite GS:Set GhS:S.Finiteh:Subgroup.closure S = ⊤this:(n : ℕ) → Fintype ↑(CayleyBall S n)A:Finset GhA:A.Nonemptyn:↥A → ℕhn:∀ (a : ↥A), ↑a ∈ CayleyBall S (n a)N:ℕ := (Set.range n).toFinset.max' ⋯a:Gha:a ∈ A⊢ a ∈ (CayleyBall S N).toFinset
simpa using cayleyBall_monotone S (Finset.le_max' _ _ (G:Type u_1inst✝¹:Group Ginst✝:Infinite GS:Set GhS:S.Finiteh:Subgroup.closure S = ⊤this:(n : ℕ) → Fintype ↑(CayleyBall S n)A:Finset GhA:A.Nonemptyn:↥A → ℕhn:∀ (a : ↥A), ↑a ∈ CayleyBall S (n a)N:ℕ := (Set.range n).toFinset.max' ⋯a:Gha:a ∈ A⊢ n ⟨a, ha⟩ ∈ (Set.range n).toFinset All goals completed! 🐙)) (hn ⟨a, ha⟩)A group has polynomial growth if there exists a finite generating set whose growth function is bounded above by a polynomial.
def HasPolynomialGrowth (G : Type*) [Group G] : Prop :=
∃ (S : Set G), Set.Finite S ∧ Subgroup.closure S = ⊤ ∧
∃ (C : ℝ) (d : ℕ), C > 0 ∧
∀ n > 0, (GrowthFunction S n : ℝ) ≤ C * (n : ℝ) ^ dA group has superpolynomial growth if there exists a finite generating set whose growth function eventually dominates every polynomial in the growth-function preorder, up to linearly rescaling the radius.
def HasSuperPolynomialGrowth (G : Type*) [Group G] : Prop :=
∃ (S : Set G), Set.Finite S ∧ Subgroup.closure S = ⊤ ∧
∀ d : ℕ, ∃ C : ℕ, 0 < C ∧
∀ᶠ n : ℕ in atTop, (n : ℝ) ^ d ≤ (GrowthFunction S (C * n) : ℝ)end GromovPolynomialGrowth