Mission

Erschler–Zheng: growth of periodic Grigorchuk groupsResearch Paper

Group Theory Probability·Captain: dbenbenn

This mission formalizes A. Erschler and T. Zheng, Growth of periodic Grigorchuk groups, Invent. Math. 219 (2020) 1069–1155 (doi:10.1007/s00222-019-00922-0). Page and result numbers are those of arXiv:1802.09077v2.

Motivation

The growth function $v_{\Gamma,S}(n)$ of a group $\Gamma$ generated by a finite set $S$ counts the elements of word length at most $n$ . A group has polynomial growth, exponential growth, or intermediate growth, strictly between the two. Grigorchuk's groups $G_\omega$ were the first groups of intermediate growth, and for forty years the precise asymptotics of their growth was open, even for the most studied of them, the first Grigorchuk group $G_{\mathbf{012}}$ . Erschler and Zheng determine its growth exponent:

\lim_{n\to\infty}\frac{\log\log v_{G,S}(n)}{\log n} = \alpha_0,

where $\alpha_0 = \log 2/\log\lambda_0 \approx 0.7674$ and $\lambda_0$ is the positive root of $X^3 - X^2 - 2X - 4$ . The upper bound was known; the new lower bound comes from random walks.

Timeline.

1980: Grigorchuk introduces the first Grigorchuk group, a finitely generated infinite periodic group (doi:10.1007/BF01078416).
1983: Kaimanovich and Vershik relate the Poisson boundary of a random walk to its asymptotic entropy (doi:10.1214/aop/1176993497); with Derriennic's work (Astérisque 74, 1980) this is the entropy criterion the lower bound rests on.
1984: Grigorchuk defines the family $G_\omega$ , proves intermediate growth, and shows $\exp(cn^{1/2}) \le v_{G,S}(n) \le \exp(Cn^{\log_{32}31})$ for $G_{\mathbf{012}}$ (doi:10.1070/IM1985v025n02ABEH001281).
1997: Leonov raises the lower exponent to $0.504$ (Mat. Stud. 8 (1997) 192–197; no DOI).
1998: Bartholdi proves $v_{G,S}(n) \le \exp(Cn^{\alpha_0})$ (doi:10.1155/S1073792898000622); Muchnik and Pak prove upper bounds of this kind for more general $\omega$ in 2001 (doi:10.1142/S0218196701000450).
2001: Bartholdi raises the lower exponent to $0.5157$ (doi:10.1142/S0218196701000395); Brieussel's thesis (2008) reaches $0.5207$ .
2020: Erschler and Zheng prove $v_{G,S}(n) \ge \exp(c_\epsilon n^{\alpha_0 - \epsilon})$ , matching Bartholdi's upper bound.

Setting

$\mathsf T$ is the rooted binary tree, its vertices the finite words over $\{0, 1\}$ and its boundary $\partial\mathsf T$ the infinite rays; automorphisms act on the right, $x \mapsto x \cdot g$ . For a string $\omega = \omega_0\omega_1\ldots \in \{\mathbf 0, \mathbf 1, \mathbf 2\}^{\mathbb N}$ , the Grigorchuk group $G_\omega$ is generated by certain automorphisms of $\mathsf T$ , $S = \{a, b_\omega, c_\omega, d_\omega\}$ . The automorphism $a$ changes the first letter of a word, swapping the two subtrees of the root, while $b_\omega, c_\omega, d_\omega$ are defined as follows. They fix $1^\infty$ , and on a word $1^k0v$ each of them either changes the first letter of $v$ or does nothing, depending on the letter $\omega_k$ of the string: if $\omega_k = \mathbf 0$ , then $b_\omega$ and $c_\omega$ change it and $d_\omega$ does nothing; if $\omega_k = \mathbf 1$ , then $b_\omega$ and $d_\omega$ change it and $c_\omega$ does nothing; if $\omega_k = \mathbf 2$ , then $c_\omega$ and $d_\omega$ change it and $b_\omega$ does nothing. The string $\omega = (\mathbf{012})^\infty$ gives the first Grigorchuk group.

Assumption $\mathrm{Fr}(D)$ asks that every block $\omega_{kD}\ldots\omega_{kD+D-1}$ contain $\mathbf{201}$ or $\mathbf{211}$ ; it implies that $G_\omega$ is periodic. $L^\omega_n$ is the sum of the entries of $M_{\omega_0}\cdots M_{\omega_{n-1}}$ for three explicit $3\times 3$ matrices: the lengths of the words the substitutions of §2 produce.

A measure on a group is a function $\mu \ge 0$ of total mass 1. A function $f$ is $\mu$ -harmonic if $f(x) = \sum_y f(xy)\mu(y)$ , the entropy is $H(\mu) = -\sum_g \mu(g)\log\mu(g)$ , and the Poisson boundary of $(\Gamma, \mu)$ is non-trivial when some bounded $\mu$ -harmonic function is not constant.

Formalization targets

Goal: Theorem 8.3 (pp. 58), with the exponent the proof gives

For every $\epsilon > 0$ there is $C > 0$ such that for every $\omega$ satisfying $\mathrm{Fr}(D)$ there is a non-degenerate symmetric probability $\mu$ on $G_\omega$ of finite entropy and non-trivial Poisson boundary with, writing $l_S$ for the word length,

\mu\{g : l_S(g) > L^\omega_n\} \le C\,2^{-(1-\epsilon)n} \quad (n \ge 1),

and hence, for some $c > 0$ depending on $\omega$ ,

v_{G_\omega,S}(L^\omega_n) \ge \exp\bigl(c\,2^{(1-\epsilon)n}\bigr) \quad (n \ge 1).

The printed theorem has $n$ in place of $2^n$ ; that version is weaker and does not give the exponent.

The abstract's headline, that the volume exponent of the first Grigorchuk group is $\alpha_0$ , is the last milestone, ErschlerZheng.hasVolumeExponent_firstString_alpha0: Theorem A combined with Bartholdi's upper bound.

Milestones

§2: the entropy criterion and the Shannon theorem for random walks (Kaimanovich–Vershik, external), the Avez entropy, and Lemma 2.1: a finite-entropy measure with non-trivial boundary forces $v_{\Gamma,S}(n\phi(\varrho_n)) \ge e^{cn}$ for all large $n$ .
§3: germs of the action on $\partial\mathsf T$ , the groupoid $\mathcal H(H_o)$ , Fact 3.5, and Proposition 3.3: if the walk's germ at $1^\infty$ stabilizes modulo a proper subgroup, the Poisson boundary is non-trivial.
§§2.4–2.5, 5, 7.1: the groups $G_\omega$ and their substitutions, the Schreier graph of $1^\infty$ and its Gray-code distance, cube independence, Facts 7.3–7.6 and Lemma 7.5.
§7.2–7.6: the conjugated elements $\tilde g^v_j$ and the measures $\mu_\beta$ (Lemmas 7.7, 7.9), kernel and Green-function bounds (Propositions 7.11, 7.12, 7.18, 7.19, Lemmas 7.15–7.17, 7.21), and Theorem 7.13: $\mu_\beta$ has non-trivial Poisson boundary.
§8: Lemma 8.1, Corollary 8.2, the goal, and after it Theorem A and the exponent of $G_{\mathbf{012}}$ , with Bartholdi's upper bound as an external milestone.

Significance

The result. It answers the growth question for $G_{\mathbf{012}}$ : the exponent is $\alpha_0$ . It gives near-optimal lower bounds for every $G_\omega$ with $\omega$ satisfying $\mathrm{Fr}(D)$ , and its measures are the first examples on these groups of random walks with non-trivial Poisson boundary and power-law tails. The method, building a measure with non-trivial boundary and controlled tail and reading off a volume bound from entropy, applies beyond Grigorchuk groups.

Formalizing it. No machine-checked proof of these results exists; Mathlib has neither Grigorchuk groups nor Poisson boundaries. On this platform the mission builds on the published bundle of the first Grigorchuk group, Garrido_Grigorchuk, from the Garrido Amenable Groups III mission, and on Chou's word balls, Chou_Growth. The general Markov-chain inputs (Cheeger, Faber–Krahn and Nash inequalities, and off-diagonal heat-kernel bounds) are separate standalone theorems.

Difficulty

Lower bounds by anti-contraction of word lengths (Grigorchuk, Leonov, Bartholdi, Brieussel) stall well below $\alpha_0$ . The entropy route needs a measure with non-trivial Poisson boundary, but on a group of subexponential growth every finitely supported symmetric measure has trivial boundary. The measure must therefore have heavy tails, and the lower bound it gives is only as good as its tail decay. The difficulty is to make the tails as light as $\alpha_0$ allows while keeping the boundary non-trivial. That needs a non-homogeneous random walk on the Schreier graph of $1^\infty$ to be transient enough to fix the germ at $1^\infty$ , and heat-kernel bounds for jump processes that are not translation invariant.

Formalization scope

Tree automorphisms are permutations of finite words (Garrido.BinaryTreeAut), acting on rays on the right by $x \cdot g = g^{-1}(x)$ , so that $x \cdot (gh) = (x \cdot g) \cdot h$ . A measure is a function $G \to \mathbb R$ summed with tsum; it is symmetric when $\mu(g^{-1}) = \mu(g)$ , and non-degenerate when its support generates $G$ as a semigroup. The Poisson boundary is non-trivial (HasNontrivialPoissonBoundary) when some bounded harmonic function is not constant on the submonoid generated by the support of $\mu$ ; for the non-degenerate measures of the goal this is the criterion of p. 2 (ErschlerZheng.hasNontrivialPoissonBoundary_iff_exists_bounded_isHarmonic_ne_of_isNondegenerate). Growth is evaluated at real radii. The definitions are in the bundles ErschlerZheng_Walks, ErschlerZheng_Germs, ErschlerZheng_Grigorchuk and ErschlerZheng_Construction.

Where a statement departs from the print, its milestone description says so: under Correction when the printed claim is false or undefined ((2.3), the substitutions on p. 15, Fact 3.5, the Gray code on p. 34, Fact 7.3, $(\mathbf{012})^\infty \in \mathrm{Fr}(3)$ on p. 59, Lemmas 7.9, 7.17 and 7.21, Propositions 7.12 and 7.18, and the uniform digits on p. 55), and under Formalization note when it reads the print or strengthens it (Lemma 2.1, Proposition 7.19, Corollary 8.2, and the constants $\lambda_0$ and $\alpha_0$ ). The goal is Theorem 8.3 with the $2^n$ its proof gives, as above.

The goal is not trivial: its measure must be a non-degenerate symmetric probability on $G_\omega$ , and the growth bound is about the generating set $S$ itself.

Reusable beyond this mission: Grigorchuk groups $G_\omega$ for every $\omega$ with their substitutions, germ groupoids of group actions, entropy and the Poisson boundary of random walks.

What is left out. Theorems B and C, Corollary 8.4 and the other applications in §8 to general $\omega$ , which need the upper bounds of Bartholdi and Erschler (doi:10.5802/aif.2902); the side results of §§4–6 on the first Grigorchuk group (Theorem 5.7 and the critical constant of recurrence); the illustrative Examples 2.4 and 7.10; and the remarks and questions of §9. They are planned for a sequel mission.

Selected references

A. Erschler, T. Zheng, Growth of periodic Grigorchuk groups, Invent. Math. 219 (2020) 1069–1155. doi:10.1007/s00222-019-00922-0; arXiv:1802.09077
R. I. Grigorchuk, Burnside's problem on periodic groups, Funct. Anal. Appl. 14 (1980) 41–43. doi:10.1007/BF01078416
R. I. Grigorchuk, Degrees of growth of finitely generated groups, and the theory of invariant means, Math. USSR-Izv. 25 (1985) 259–300. doi:10.1070/IM1985v025n02ABEH001281
V. A. Kaimanovich, A. M. Vershik, Random walks on discrete groups: boundary and entropy, Ann. Probab. 11 (1983) 457–490. doi:10.1214/aop/1176993497
Y. Derriennic, Quelques applications du théorème ergodique sous-additif, Astérisque 74 (1980) 183–201. numdam
L. Bartholdi, The growth of Grigorchuk's torsion group, Internat. Math. Res. Notices 1998, no. 20, 1049–1054. doi:10.1155/S1073792898000622
R. Muchnik, I. Pak, On growth of Grigorchuk groups, Internat. J. Algebra Comput. 11 (2001) 1–17. doi:10.1142/S0218196701000450
L. Bartholdi, Lower bounds on the growth of a group acting on the binary rooted tree, Internat. J. Algebra Comput. 11 (2001) 73–88. doi:10.1142/S0218196701000395
M. T. Barlow, A. Grigor'yan, T. Kumagai, Heat kernel upper bounds for jump processes and the first exit time, J. Reine Angew. Math. 626 (2009) 135–157. doi:10.1515/CRELLE.2009.005
L. Bartholdi, A. Erschler, Groups of given intermediate word growth, Ann. Inst. Fourier 64 (2014) 2003–2036. doi:10.5802/aif.2902

Goal · Theorem 8.3, with 2^n as proved — under Fr(D), for ε > 0 a non-degenerate symmetric finite-entropy μ on G_ω with non-trivial boundary, μ(B(id, L^ω_n)^c) ⩽ C2^{−(1−ε)n} and v(L^ω_n) ⩾ exp(c2^{(1−ε)n})

PROVED

namespace ErschlerZheng

theorem exists_measure_mass_compl_ball_le_and_exp_le_growth_of_satisfiesFr (D : ℕ) (ε : ℝ)
    (hε : 0 < ε) :
    ∃ C > (0 : ℝ), ∀ ω : ℕ → Fin 3, SatisfiesFr D ω →
      ∃ μ : grigorchuk ω → ℝ, IsNondegenerate μ ∧ IsSymmetric μ ∧ IsProbability μ ∧
        HasFiniteEntropy μ ∧ HasNontrivialPoissonBoundary μ ∧
        (∀ n : ℕ, 1 ≤ n →
          mass μ (ball (genSet ω) (lengthL ω n))ᶜ ≤ C * (2 : ℝ) ^ (-((1 - ε) * n))) ∧
        ∃ c > (0 : ℝ), ∀ n : ℕ, 1 ≤ n →
          Real.exp (c * (2 : ℝ) ^ ((1 - ε) * n)) ≤ growth (genSet ω) (lengthL ω n) := by
  sorry

end ErschlerZheng

Let $\epsilon > 0$ . Then there is $C > 0$ such that for every string $\omega$ satisfying Assumption $(\mathrm{Fr}(D))$ (SatisfiesFr) there is a function $\mu$ on $G_\omega$ (grigorchuk ω) that is a non-degenerate (IsNondegenerate), symmetric (IsSymmetric) probability (IsProbability) of finite entropy (HasFiniteEntropy) with non-trivial Poisson boundary (HasNontrivialPoissonBoundary), such that

\mu\bigl(B(id, L^\omega_n)^c\bigr) \le C\,2^{-(1-\epsilon)n} \quad \text{for every } n \ge 1,

and there is $c > 0$ with

v_{G_\omega,S}(L^\omega_n) \ge \exp\bigl(c\,2^{(1-\epsilon)n}\bigr) \quad \text{for every } n \ge 1.

Here $S = \{a, b_\omega, c_\omega, d_\omega\}$ (genSet ω), $B(id, R)$ is the ball of radius $R$ (ball), $v_{G_\omega,S}$ is the growth function (growth), and $L^\omega_n$ is the number (8.1) (lengthL).

Erschler and Zheng, p. 58, Theorem 8.3: “Let $\omega$ be a string satisfying Assumption $(\mathrm{Fr}(D))$ . For any $\epsilon > 0$ , there exists a constant $C = C(D, \epsilon) > 0$ and a non-degenerate symmetric probability measure $\mu$ on $G_\omega$ of finite entropy and nontrivial Poisson boundary with tail decay $\mu(B(id, L^\omega_n)^c) \leqslant Cn^{-1+\epsilon}$ , where the number $L^\omega_n$ is defined in (8.1). As a consequence, there exists constant $c = c(\omega, \epsilon) > 0$ such that for all $n \geqslant 1$ , $v_{G_\omega,S}(L^\omega_n) \geqslant \exp(cn^{1-\epsilon})$ .”

The proof gives $2^n$ where the statement prints $n$ . The proof gives $\mu_\beta(B(id, n^{2A}L^\omega_n)^c) \le C/2^{n\beta}$ with $\beta > 1 - \epsilon$ (p. 58; the milestone ErschlerZheng.isProbability_and_hasFiniteEntropy_muBeta_and_mass_ball_compl_le, at the radius $2^{2k_n}L^\omega_n$ ), and since $L^\omega_{n+1} \ge 2L^\omega_n$ (ErschlerZheng.two_mul_lengthL_le_lengthL_succ) that is the tail bound $C\,2^{-(1-\epsilon)n}$ at the radius $L^\omega_n$ ; Lemma 2.1 (ErschlerZheng.exp_le_growth_of_hasNontrivialPoissonBoundary) then gives $\exp(c\,2^{(1-\epsilon)n})$ . The statement asserts that form; the printed bounds, weaker for $\epsilon \le 1$ , are stated as printed in ErschlerZheng.exists_measure_mass_compl_ball_le_rpow_and_exp_le_growth_of_satisfiesFr.

Theorem A needs the stronger form. The paper obtains it as “the special case of Theorem 8.3 applied to the periodic sequence $(\mathbf{012})^\infty$ ” (p. 59), and its exponent $\alpha_0 = \log 2/\log\lambda_0$ comes from comparing $2^n$ with $L^\omega_n \le 3\lambda_0^n$ for $\omega = (\mathbf{012})^\infty$ (ErschlerZheng.lengthL_firstString_le_three_mul_lambda0_pow). The printed bounds are powers of $n$ , and $L^\omega_n \ge 3 \cdot 2^n$ (ErschlerZheng.two_mul_lengthL_le_lengthL_succ), so they are powers of $\log L^\omega_n$ and give no exponent.

$C$ is chosen before $\omega$ , as $C = C(D, \epsilon)$ says, and $c$ after $\omega$ and $\mu$ , as $c = c(\omega, \epsilon)$ says. The tail bound is asserted for $n \ge 1$ , the range of the printed consequence. A measure on $G_\omega$ is a function $G_\omega \to \mathbb R$ (Walks bundle note).

Erschler–Zheng: growth of periodic Grigorchuk groupsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8.3 (pp. 58), with the exponent the proof gives

Milestones

Significance

Difficulty

Formalization scope

Selected references

Frontier · Open leaf nodes

Recent activity

Erschler–Zheng: growth of periodic Grigorchuk groups

Frontier · Open leaf nodes

Recent activity

Erschler–Zheng: growth of periodic Grigorchuk groupsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8.3 (pp. 58), with the exponent the proof gives

Milestones

Significance

Difficulty

Formalization scope

Selected references

Frontier · Open leaf nodes

Recent activity

Frontier · Open leaf nodes

Recent activity

Frontier · Open leaf nodes

Recent activity