Wrapping up

TheoremEntropy form of PFR#

Suppose that \(G\) is a finite abelian group of torsion \(m\). Suppose that \(X\) is a \(G\)-valued random variable. Then there exists a subgroup \(H \leq G\) such that

\[ d[X;U_H] \leq 64 m^3 d[X;X]. \]
Proof

Set \(X^0 := X\). By Existence of \(\tau\)-minimizer, there exists a \(\tau\)-minimizer \(X_{[m]} = (X_i)_{1 \leq i \leq m}\). By Vanishing entropy, we have \(D[X_{[m]}]=0\). By Minimizer close to reference variables and the pigeonhole principle, there exists \(1 \leq i \leq m\) such that \(d[X_i; X] \leq \frac{2}{\eta} d[X;X]\). By Vanishing, we have \(d[X_i;U_H]=0\) for some subgroup \(H \leq G\), hence by Ruzsa triangle inequality we have \(d[U_H; X] \leq \frac{2}{\eta} d[X;X]\). The claim then follows from \(\eta\).

Lean

Formalized as dist_of_X_U_H_le.

Sources
Leandist_of_X_U_H_le
Uses 7 · Used by 1
Proof usesVanishing entropy · Ruzsa triangle inequality · \(\tau\) functional · Vanishing · \(\eta\) · Minimizer close to reference variables · Existence of \(\tau\)-minimizer
Used bypfr_aux_torsion

Lemmapfr_aux_torsion#

Suppose that \(G\) is a finite abelian group of torsion \(m\). If \(A \subset G\) is non-empty and \(|A+A| \leq K|A|\), then \(A\) can be covered by at most \(K ^ {128m^3+1}|A|^{1/2}/|H|^{1/2}\) translates of a subspace \(H\) of \(G\) with

\[ |H|/|A| \in [K^{-256m^3}, K^{256m^3}].\qquad\text{(1)} \]
Proof

Repeat the proof of Lemma pfr_aux, but with Entropy form of PFR in place of Entropy version of PFR. Because of the lack of \(2\)-torsion, one has to use the Ruzsa triangle inequality to bound \(d[U,U]\) by \(2d[U,-U]\), costing an additional factor of \(2\) in the estimates.

Lean

Formalized as torsion_PFR_conjecture_aux.

Sources
Leantorsion_PFR_conjecture_aux
Uses 8 · Used by 1
Proof usesEntropy form of PFR · Uniform distributions exist · Entropy of uniform random variable, II · Jensen bound · Ruzsa distance · Distance controls entropy difference · Bounded entropy implies concentration · Ruzsa covering lemma
Used byPFR

TheoremPFR#

Suppose that \(G\) is an abelian group of torsion \(m\) (not necessarily finite). If \(A \subset G\) is a finite non-empty set with \(|A+A| \leq K|A|\), then \(A\) can be covered by at most \(mK^{256m^3+1}\) translates of a finite subspace \(H\) of \(G\) with \(|H| \leq |A|\).

Proof

If \(G\) is finite, repeat the proof of PFR, but with Lemma pfr_aux_torsion in place of Lemma pfr_aux. In general, reduce to the finite span of \(A\) over \(\mathrm{Z}/m\mathrm{Z}\).

Lean

Formalized as torsion_PFR.

Sources
Leantorsion_PFR
Uses 1
Proof usespfr_aux_torsion

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.