Proof of PFR

LemmaRuzsa covering lemma#

If \(A,B\) are finite non-empty subsets of a group \(G\), then \(A\) can be covered by at most \(|A+B|/|B|\) translates of \(B-B\).

Proof

Cover \(A\) greedily by disjoint translates of \(B\).

Lean

Formalized as Finset.ruzsa_covering_add.

Sources
LeanFinset.ruzsa_covering_add
Used by 5
Used byPFR with \(C=9\) · pfr-9-aux' · pfr_aux-improv · pfr_aux · pfr_aux_torsion

Lemmapfr_aux#

If \(A \subset {\bf F}_2^n\) is non-empty and \(|A+A| \leq K|A|\), then \(A\) can be covered by at most \(K ^ {13/2}|A|^{1/2}/|H|^{1/2}\) translates of a subspace \(H\) of \({\bf F}_2^n\) with

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

Let \(U_A\) be the uniform distribution on \(A\) (which exists by Uniform distributions exist), thus \(\mathbb{H}[U_A] = \log |A|\) by Entropy of uniform random variable, II. By Jensen bound and the fact that \(U_A + U_A\) is supported on \(A + A\), \(\mathbb{H}[U_A + U_A] \leq \log|A+A|\). By Ruzsa distance, the doubling condition \(|A+A| \leq K|A|\) therefore gives

\[ d[U_A;U_A] \leq \log K. \]

By Entropy version of PFR, we may thus find a subspace \(H\) of \(\mathbb{F}_2^n\) such that

\[ d[U_A;U_H] \leq \tfrac{1}{2} C' \log K\qquad\text{(2)} \]

with \(C' = 11\). By Distance controls entropy difference we conclude that

\[ |\log |H| - \log |A|| \leq C' \log K, \]

proving (1). From Ruzsa distance, (2) is equivalent to

\[ \mathbb{H}[U_A - U_H] \leq \log( |A|^{1/2} |H|^{1/2}) + \tfrac{1}{2} C' \log K. \]

By Bounded entropy implies concentration we conclude the existence of a point \(x_0 \in \mathbb{F}_p^n\) such that

\[ p_{U_A-U_H}(x_0) \geq |A|^{-1/2} |H|^{-1/2} K^{-C'/2}, \]

or equivalently

\[ |A \cap (H + x_0)| \geq K^{-C'/2} |A|^{1/2} |H|^{1/2}. \]

Applying Ruzsa covering lemma, we may thus cover \(A\) by at most

\[ \frac{|A + (A \cap (H+x_0))|}{|A \cap (H + x_0)|} \leq \frac{K|A|}{K^{-C'/2} |A|^{1/2} |H|^{1/2}} = K^{C'/2+1} \frac{|A|^{1/2}}{|H|^{1/2}} \]

translates of

\[ \bigl(A \cap (H + x_0)\bigr) - \bigl(A \cap (H + x_0)\bigr) \subseteq H. \]

This proves the claim.

Lean

Formalized as PFR_conjecture_aux.

Sources
LeanPFR_conjecture_aux
Uses 8 · Used by 1
Proof usesEntropy version 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#

If \(A \subset {\bf F}_2^n\) is non-empty and \(|A+A| \leq K|A|\), then \(A\) can be covered by most \(2K^{12}\) translates of a subspace \(H\) of \({\bf F}_2^n\) with \(|H| \leq |A|\).

Proof

Let \(H\) be given by Lemma pfr_aux. If \(|H| \leq |A|\) then we are already done thanks to (1). If \(|H| > |A|\) then we can cover \(H\) by at most \(2 |H|/|A|\) translates of a subspace \(H'\) of \(H\) with \(|H'| \leq |A|\). We can thus cover \(A\) by at most

\[ 2K^{13/2} \frac{|H|^{1/2}}{|A|^{1/2}} \]

translates of \(H'\), and the claim again follows from (1).

Lean

Formalized as PFR_conjecture.

Sources
LeanPFR_conjecture
Uses 1 · Used by 1
Proof usespfr_aux
Used byPFR in infinite groups

CorollaryPFR in infinite groups#

If \(G\) is an abelian \(2\)-torsion group, \(A \subset G\) is non-empty finite, and \(|A+A| \leq K|A|\), then \(A\) can be covered by most \(2K^{12}\) translates of a finite group \(H\) of \(G\) with \(|H| \leq |A|\).

Proof

Apply PFR to the group generated by \(A\), which is isomorphic to \(\mathbb{F}_2^n\) for some \(n\).

Lean

Formalized as PFR_conjecture.

Sources
LeanPFR_conjecture
Uses 1
Proof usesPFR

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.