Growth of groups

DefinitionGrowth function of a generating family#✓fully proved

Let \(P\) be a generating family of a group \(G\). The growth function \(\gamma_P\) of \(P\) assigns to each natural number \(n\) the number of elements \(g \in G\) whose word length with respect to \(P\) is at most \(n\), that is, the cardinality of the ball of radius \(n\) in the word metric of \(P\); when this ball is infinite, \(\gamma_P(n)\) is taken to be \(0\).

noncomputable def growth (n : ℕ) : ℕ := Nat.card {g : G // P.wordLength g ≤ n}
Used by 6
Used byThe growth function is bounded by the order of the group · The growth function of a finite group is positive · Polynomial growth makes the growth function positive · The growth function at radius zero · Polynomial growth · Finite groups have polynomial growth

DefinitionPolynomial growth#✓fully proved

Let \(P\) be a generating family of a group \(G\), with growth function \(\gamma_P\). Then \(P\) has polynomial growth if, for every natural number \(n\), the ball of radius \(n\) (the set of elements of \(G\) of word length at most \(n\) with respect to \(P\)) is finite, and there are natural numbers \(C\) and \(d\) such that \(\gamma_P(n) \le C (n + 1)^d\) for every natural number \(n\).

def HasPolynomialGrowth : Prop :=
  (∀ n, Finite {g : G // P.wordLength g ≤ n}) ∧
    ∃ C d : ℕ, ∀ n, P.growth n ≤ C * (n + 1) ^ d
Uses 1 · Used by 3
Statement usesGrowth function of a generating family
Used byGroups of intermediate growth · Polynomial growth makes the growth function positive · Finite groups have polynomial growth

LemmaThe growth function at radius zero#✓fully proved

For every generating family \(P\) of a group \(G\), the growth function of \(P\) takes the value \(1\) at \(0\): the ball of radius \(0\) consists of the identity element alone.

lemma growth_zero : P.growth 0 = 1
Uses 1
Statement usesGrowth function of a generating family

LemmaThe growth function of a finite group is positive#✓fully proved

For every generating family \(P\) of a finite group \(G\) and every natural number \(n\), the growth function of \(P\) is positive at \(n\): the ball of radius \(n\) contains the identity.

lemma growth_pos [Finite G] (n : ℕ) : 0 < P.growth n
Uses 1
Statement usesGrowth function of a generating family

LemmaThe growth function is bounded by the order of the group#✓fully proved

For every generating family \(P\) of a finite group \(G\) and every natural number \(n\), the value of the growth function of \(P\) at \(n\) is at most the order of \(G\), since every ball is a subset of \(G\).

lemma growth_le_card [Finite G] (n : ℕ) : P.growth n ≤ Nat.card G
Uses 1 · Used by 1
Statement usesGrowth function of a generating family
Used byFinite groups have polynomial growth

TheoremFinite groups have polynomial growth#✓fully proved

Every generating family of a finite group has polynomial growth: its growth function is bounded by the order of the group, a polynomial of degree \(0\).

theorem hasPolynomialGrowth_of_finite [Finite G] : P.HasPolynomialGrowth
Uses 3
Statement usesPolynomial growth
Proof usesGrowth function of a generating family · The growth function is bounded by the order of the group

LemmaPolynomial growth makes the growth function positive#✓fully proved

If a generating family \(P\) of a group \(G\) has polynomial growth, then the growth function of \(P\) is positive at every natural number \(n\).

lemma HasPolynomialGrowth.growth_pos (h : P.HasPolynomialGrowth) (n : ℕ) : 0 < P.growth n
Uses 2
Statement usesPolynomial growth · Growth function of a generating family
7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.