Gap conjecture #
References:
- Wikipedia
- On the Gap Conjecture concerning group growth by Rostislav Grigorchuk
theorem
GapConjecture.gap_conjecture
(G : Type)
[Group G]
(S : Set G)
:
S.Finite →
Subgroup.closure S = ⊤ →
GromovPolynomialGrowth.HasSuperPolynomialGrowth G →
∃ (C : ℕ), 0 < C ∧ ∀ᶠ (n : ℕ) in Filter.atTop, Real.exp √↑n ≤ ↑(GromovPolynomialGrowth.GrowthFunction S (C * n))
If a finitely generated group has superpolynomial growth, then with respect to any finite generating set its growth function is at least $e^{\sqrt n}$ in Grigorchuk's preorder on growth functions, where the comparison is witnessed by linearly rescaling the radius.