def GromovPolynomialGrowth.CayleyBall {G : Type u_1} [Group G] (S : Set G) (n : ℕ) : Set G

The CayleyBall is the ball of radius n in the Cayley graph of a group G with generating set S.

Equations

• GromovPolynomialGrowth.CayleyBall S n = {g : G | ∃ (l : List G), l.length ≤ n ∧ (∀ s ∈ l, s ∈ S ∨ s⁻¹ ∈ S) ∧ l.prod = g}

theorem GromovPolynomialGrowth.cayleyBall_zero {G : Type u_1} [Group G] (S : Set G) : CayleyBall S 0 = {1}

theorem GromovPolynomialGrowth.cayleyBall_finite {G : Type u_1} [Group G] {S : Set G} (hS : S.Finite) (n : ℕ) : (CayleyBall S n).Finite

noncomputable def GromovPolynomialGrowth.GrowthFunction {G : Type u_1} [Group G] (S : Set G) (n : ℕ) : ℕ

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.

Equations

• GromovPolynomialGrowth.GrowthFunction S n = (GromovPolynomialGrowth.CayleyBall S n).ncard

theorem GromovPolynomialGrowth.growthFunction_zero {G : Type u_1} [Group G] (S : Set G) : GrowthFunction S 0 = 1

theorem GromovPolynomialGrowth.one_mem_cayleyBall {G : Type u_1} [Group G] (S : Set G) (n : ℕ) : 1 ∈ CayleyBall S n

The identity is always in the Cayley ball.

theorem GromovPolynomialGrowth.cayleyBall_monotone {G : Type u_1} [Group G] (S : Set G) {m n : ℕ} (h : m ≤ n) : CayleyBall S m ⊆ CayleyBall S n

The Cayley ball is monotonic in its radius.

theorem GromovPolynomialGrowth.cayleyBall_mul {G : Type u_1} [Group G] (S : Set G) {g h : G} {m n : ℕ} (hg : g ∈ CayleyBall S m) (hh : h ∈ CayleyBall S n) : g * h ∈ CayleyBall S (m + n)

Closure property: if g ∈ CayleyBall S m and h ∈ CayleyBall S n, then g * h ∈ CayleyBall S (m + n).

theorem GromovPolynomialGrowth.cayleyBall_inv {G : Type u_1} [Group G] (S : Set G) {g : G} {n : ℕ} (hg : g ∈ CayleyBall S n) : g⁻¹ ∈ CayleyBall S n

If g ∈ CayleyBall S n, then g⁻¹ ∈ CayleyBall S n.

theorem GromovPolynomialGrowth.mem_cayleyBall_one_of_mem {G : Type u_1} [Group G] {S : Set G} {g : G} (hg : g ∈ S) : g ∈ CayleyBall S 1

theorem GromovPolynomialGrowth.exists_cayleyBall_mem_of_closure_eq_top {G : Type u_1} [Group G] {S : Set G} (h : Subgroup.closure S = ⊤) (g : G) : ∃ (n : ℕ), g ∈ CayleyBall S n

theorem GromovPolynomialGrowth.tendsto_atTop_growthFunction_of_infinite {G : Type u_1} [Group G] [Infinite G] {S : Set G} (hS : S.Finite) (h : Subgroup.closure S = ⊤) : Filter.Tendsto (GrowthFunction S) Filter.atTop Filter.atTop

In an infinite group, the growth function with respect to a finite generating set is unbounded.

def GromovPolynomialGrowth.HasPolynomialGrowth (G : Type u_2) [Group G] : Prop

A group has polynomial growth if there exists a finite generating set whose growth function is bounded above by a polynomial.

Equations

• One or more equations did not get rendered due to their size.

def GromovPolynomialGrowth.HasSuperPolynomialGrowth (G : Type u_2) [Group G] : Prop

A 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.

Equations

• One or more equations did not get rendered due to their size.