Studying a minimizer

Set \(\eta < 1/8\). In this section, consider \(G=\mathbb{F}_2^n\).

Definitionphi-min-def#

Given \(G\)-valued random variables \(X,Y\), define

\[ \phi[X;Y] := d[X;Y] + \eta(\rho(X) + \rho(Y)) \]

and define a \(\phi\)-minimizer to be a pair of random variables \(X,Y\) which minimizes \(\phi[X;Y]\).

Lean

Formalized as phiMinimizes.

Sources
LeanphiMinimizes
Used by 4
Used bypfr-rho · phi-first-estimate · phi-second-estimate · rho-BSG-triplet

Lemma\(\phi\)-minimizers exist#

There exists a \(\phi\)-minimizer.

Proof

Clear from compactness.

Lean

Formalized as phi_min_exists.

Sources
Leanphi_min_exists
Uses 1 · Used by 1
Proof usesRho continuous
Used bypfr-rho

Let \((X_1, X_2)\) be a \(\phi\)-minimizer, and \(\tilde X_1, \tilde X_2\) be independent copies of \(X_1,X_2\) respectively. Similar to the original proof we define

\[ I_1 := I [X_1+X_2 : \tilde X_1 + X_2 | X_1+X_2+\tilde X_1+\tilde X_2], I_2 := \mathbb{I}[X_1+X_2 : X_1 + \tilde X_1 | X_1+X_2+\tilde X_1+\tilde X_2]. \]

First we need the \(\phi\)-minimizer variants of First estimate and Second estimate.

Lemmaphi-first-estimate#

\(I_1\le 2\eta d[X_1;X_2]\)

Proof

Similar to First estimate: get upper bounds for \(d[X_1;X_2]\) by \(\phi[X_1;X_2]\le \phi[X_1+X_2;\tilde X_1+\tilde X_2]\) and \(\phi[X_1;X_2]\le \phi[X_1|X_1+X_2;\tilde X_2|\tilde X_1+\tilde X_2]\), and then apply Fibring identity for first estimate to get an upper bound for \(I_1\).

Lean

Formalized as I_one_le.

Sources
LeanI_one_le
Uses 2 · Used by 1
Proof usesphi-min-def · Fibring identity for first estimate
Used byphi-minimizer-zero-distance

LemmaI1-I2-diff#

\(d[X_1;X_1]+d[X_2;X_2]= 2d[X_1;X_2]+(I_2-I_1)\).

Proof

Compare Fibring identity for first estimate with the identity obtained from applying Specific fibring identity on \((X_1,\tilde X_1, X_2, \tilde X_2)\).

Lean

Formalized as rdist_add_rdist_eq.

Sources
Leanrdist_add_rdist_eq
Uses 2 · Used by 2
Proof usesFibring identity for first estimate · Specific fibring identity
Used byphi-minimizer-zero-distance · phi-second-estimate

Lemmaphi-second-estimate#

\(I_2\le 2\eta d[X_1;X_2] + \frac{\eta}{1-\eta}(2\eta d[X_1;X_2]-I_1)\).

Proof

First of all, by \(\phi[X_1;X_2]\le \phi[X_1+\tilde X_1;X_2+\tilde X_2]\), \(\phi[X_1;X_2]\le \phi[X_1|X_1+\tilde X_1;X_2|X_2+\tilde X_2]\), and the fibring identity obtained by applying Specific fibring identity on \((X_1,X_2,\tilde X_1,\tilde X_2)\), we have \(I_2\le \eta (d[X_1;X_1]+d[X_2;X_2])\). Then apply Lemma I1-I2-diff to get \(I_2\le 2\eta d[X_1;X_2] +\eta(I_2-I_1)\), and rearrange.

Lean

Formalized as I_two_le.

Sources
LeanI_two_le
Uses 3 · Used by 1
Proof usesphi-min-def · Specific fibring identity · I1-I2-diff
Used byphi-minimizer-zero-distance

Next we need some inequalities for the endgame.

Lemmarho-BSG-triplet#

If \(G\)-valued random variables \(T_1,T_2,T_3\) satisfy \(T_1+T_2+T_3=0\), then

\[ d[X_1;X_2]\le 3\mathbb{I}[T_1:T_2] + (2\mathbb{H}[T_3]-\mathbb{H}[T_1]-\mathbb{H}[T_2])+ \eta(\rho(T_1|T_3)+\rho(T_2|T_3)-\rho(X_1)-\rho(X_2)). \]
Proof

Conditioned on every \(T_3=t\), \(d[X_1;X_2]\le d[T_1|T_3=t;T_2|T_3=t]+\eta(\rho(T_1|T_3=t)+\rho(T_2|T_3=t)-\rho(X_1)-\rho(X_2))\) by Definition phi-min-def. Then take the weighted average with weight \(\mathbf{P}(T_3=t)\) and then apply Balog-Szemerédi-Gowers to bound the RHS.

Lean

Formalized as dist_le_of_sum_zero.

Sources
Leandist_le_of_sum_zero
Uses 2 · Used by 1
Proof usesBalog-Szemerédi-Gowers · phi-min-def
Used byrho-BSG-triplet-symmetrized

Lemmarho-BSG-triplet-symmetrized#

If \(G\)-valued random variables \(T_1,T_2,T_3\) satisfy \(T_1+T_2+T_3=0\), then

\[ d[X_1;X_2] \leq \sum_{1 \leq i\lt j \leq 3} \mathbb{I}[T_i:T_j] + \frac{\eta}{3} \sum_{1 \leq i\lt j \leq 3} (\rho(T_i|T_j) + \rho(T_j|T_i) -\rho(X_1)-\rho(X_2)) \]
Proof

Take the average of Lemma rho-BSG-triplet over all \(6\) permutations of \(T_1,T_2,T_3\).

Lean

Formalized as dist_le_of_sum_zero'.

Sources
Leandist_le_of_sum_zero'
Uses 1 · Used by 1
Proof usesrho-BSG-triplet
Used byphi-minimizer-zero-distance

Lemmarho-increase#

For independent random variables \(Y_1,Y_2,Y_3,Y_4\) over \(G\), define \(S:=Y_1+Y_2+Y_3+Y_4\), \(T_1:=Y_1+Y_2\), \(T_2:=Y_1+Y_3\). Then

\[ \rho(T_1|T_2,S)+\rho(T_2|T_1,S) - \frac{1}{2}\sum_{i} \rho(Y_i)\le \frac{1}{2}(d[Y_1;Y_2]+d[Y_3;Y_4]+d[Y_1;Y_3]+d[Y_2;Y_4]). \]
Proof

Let \(T_1':=Y_3+Y_4\), \(T_2':=Y_2+Y_4\). First note that

\[ \begin{aligned} \rho(T_1|T_2,S) &\le \rho(T_1|S) + \frac{1}{2}\mathbb{I}(T_1:T_2\mid S) \\ &\le \frac{1}{2}(\rho(T_1)+\rho(T_1'))+\frac{1}{2}(d[T_1;T_1']+\mathbb{I}(T_1:T_2\mid S)) \\ &\le \frac{1}{4} \sum_{i} \rho(Y_i) +\frac{1}{4}(d[Y_1;Y_2]+d[Y_3;Y_4]) + \frac{1}{2}(d[T_1;T_1']+\mathbb{I}(T_1:T_2\mid S)). \end{aligned} \]

by Rho and conditioning, Rho and conditioning, symmetrized, Rho and sums, symmetrized respectively. On the other hand, observe that

\[ \begin{aligned} \rho(T_1|T_2,S) &=\rho(Y_1+Y_2|T_2,T_2') \\ &\le \frac{1}{2}(\rho(Y_1|T_2)+\rho(Y_2|T_2'))+\frac{1}{2}(d[Y_1|T_2;Y_2|T_2']) \\ &\le \frac{1}{4} \sum_{i} \rho(Y_i) +\frac{1}{4}(d[Y_1;Y_3]+d[Y_2;Y_4]) + \frac{1}{2}(d[Y_1|T_2;Y_2|T_2']). \end{aligned} \]

by Conditional rho and relabeling, Rho and sums, symmetrized, Rho and conditioning, symmetrized respectively. By replacing \((Y_1,Y_2,Y_3,Y_4)\) with \((Y_1,Y_3,Y_2,Y_4)\) in the above inequalities, one has

\[ \rho(T_2|T_1,S) \le \frac{1}{4} \sum_{i} \rho(Y_i) +\frac{1}{4}(d[Y_1;Y_3]+d[Y_2;Y_4]) + \frac{1}{2}(d[T_2;T_2']+\mathbb{I}(T_1:T_2\mid S)) \]

and

\[ \rho(T_2|T_1,S) \le \frac{1}{4} \sum_{i} \rho(Y_i) +\frac{1}{4}(d[Y_1;Y_2]+d[Y_3;Y_4]) + \frac{1}{2}(d[Y_1|T_1;Y_3|T_1']). \]

Finally, take the sum of all four inequalities, apply Specific fibring identity on \((Y_1,Y_2,Y_3,Y_4)\) and \((Y_1,Y_3,Y_2,Y_4)\) to rewrite the sum of last terms in the four inequalities, and divide the result by \(2\).

Lean

Formalized as condRho_sum_le.

Sources
LeancondRho_sum_le
Uses 5 · Used by 1
Proof usesRho and sums, symmetrized · Rho and conditioning · Rho and conditioning, symmetrized · Conditional rho and relabeling · Specific fibring identity
Used byrho-increase-symmetrized

Lemmarho-increase-symmetrized#

For independent random variables \(Y_1,Y_2,Y_3,Y_4\) over \(G\), define \(T_1:=Y_1+Y_2,T_2:=Y_1+Y_3,T_3:=Y_2+Y_3\) and \(S:=Y_1+Y_2+Y_3+Y_4\). Then

\[ \sum_{1 \leq i\lt j \leq 3} (\rho(T_i|T_j,S) + \rho(T_j|T_i,S) - \frac{1}{2}\sum_{i} \rho(Y_i))\le \sum_{1\leq i < j \leq 4}d[Y_i;Y_j] \]
Proof

Apply Lemma rho-increase on \((Y_i,Y_j,Y_k,Y_4)\) for \((i,j,k)=(1,2,3),(2,3,1),(1,3,2)\), and take the sum.

Lean

Formalized as condRho_sum_le'.

Sources
LeancondRho_sum_le'
Uses 1 · Used by 1
Proof usesrho-increase
Used byphi-minimizer-zero-distance

Propositionphi-minimizer-zero-distance#

If \(X_1,X_2\) is a \(\phi\)-minimizer, then \(d[X_1;X_2] = 0\).

Proof

Consider \(T_1:=X_1+X_2,T_2:=X_1+\tilde X_1, T_3:=\tilde X_1 + X_2\), and \(S=X_1+X_2+\tilde X_1 + \tilde X_2\). Note that \(T_1+T_2+T_3=0\). First apply Lemma rho-BSG-triplet-symmetrized on \((T_1,T_2,T_3)\) when conditioned on \(S\) to get

\[ \begin{aligned} d[X_1;X_2] &\leq \sum_{1 \leq i\lt j \leq 3} \mathbb{I}[T_i:T_j\mid S] + \frac{\eta}{3} \sum_{1 \leq i\lt j \leq 3} (\rho(T_i|T_j,S) + \rho(T_j|T_i,S) -\rho(X_1)-\rho(X_2))\qquad\text{(1)}\\ &= (I_1+2I_2) + \frac{\eta}{3} \sum_{1 \leq i\lt j \leq 3} (\rho(T_i|T_j,S) + \rho(T_j|T_i,S) -\rho(X_1)-\rho(X_2)). \end{aligned} \]

Then apply Lemma rho-increase-symmetrized on \((X_1,X_2,\tilde X_1,\tilde X_2)\) and get

\[ \sum_{1 \leq i\lt j \leq 3} (\rho(T_i|T_j,S) + \rho(T_j|T_i,S) - \rho(X_1)-\rho(X_2))\le (4d[X_1;X_2]+d[X_1;X_2]+d[X_2;X_2])= 6 d[X_1;X_2]+(I_2-I_1) \]

by Lemma I1-I2-diff. Plug in the inequality above to (1), we get

\[ d[X_1;X_2] \le (I_1+2I_2)+2\eta d[X_1;X_2]+\frac{\eta}{3}(I_2-I_1). \]

By Lemma phi-second-estimate we can conclude that

\[ d[X_1;X_2] \le 8\eta d[X_1;X_2]-\frac{3-10\eta}{3-3\eta} (2\eta d[X_1;X_2]-I_1). \]

Finally by Lemma phi-first-estimate and \(\eta<1\) we get that the second term is \(\le 0\), and thus \(d[X_1;X_2] \le 8\eta d[X_1;X_2]\). By the choice \(\eta<1/8\) and the non-negativity of \(d\) we have \(d[X_1;X_2]=0\).

Lean

Formalized as dist_of_min_eq_zero.

Sources
Leandist_of_min_eq_zero
Uses 5 · Used by 1
Proof usesrho-BSG-triplet-symmetrized · rho-increase-symmetrized · I1-I2-diff · phi-first-estimate · phi-second-estimate
Used bypfr-rho

Propositionpfr-rho#

For any random variables \(Y_1,Y_2\), there exist a subgroup \(H\) such that

\[ 2\rho(U_H) \leq \rho(Y_1) + \rho(Y_2) + 8 d[Y_1;Y_2]. \]
Proof

Let \(X_1,X_2\) be a \(\phi\)-minimizer. By Proposition phi-minimizer-zero-distance \(d[X_1;X_2]=0\), which by Definition phi-min-def implies \(\rho(X_1)+\rho(X_2)\le \rho(Y_1) + \rho(Y_2) + \frac{1}{\eta} d[Y_1;Y_2]\) for every \(\eta<1/8\). Take the limit at \(\eta=1/8\) to get \(\rho(X_1)+\rho(X_2)\le \rho(Y_1) + \rho(Y_2) + 8 d[Y_1;Y_2]\). By Ruzsa triangle inequality and Distance nonnegative we have \(d[X_1;X_1]=d[X_2;X_2]=0\), and by Translate is uniform on symmetry group there are \(H_1:=\mathrm{Sym}[X_1],H_2:=\mathrm{Sym}[X_2]\) such that \(X_1=U_{H_1}+x_1\) and \(X_2=U_{H_2}+x_2\) for some \(x_2\). By Rho invariant we get \(\rho(U_{H_1})+\rho(U_{H_2})\le \rho(Y_1) + \rho(Y_2) + 8 d[Y_1;Y_2]\), and thus the claim holds for \(H=H_1\) or \(H=H_2\).

Lean

Formalized as rho_PFR_conjecture.

Sources
Leanrho_PFR_conjecture
Uses 5 · Used by 1
Proof uses\(\phi\)-minimizers exist · phi-minimizer-zero-distance · phi-min-def · Rho invariant · Translate is uniform on symmetry group
Used bypfr-9-aux

Corollarypfr-9-aux#

If \(|A+A| \leq K|A|\), then there exists a subgroup \(H\) and \(t\in G\) such that \(|A \cap (H+t)| \geq K^{-4} \sqrt{|A||H|}\), and \(|H|/|A|\in[K^{-8},K^8]\).

Proof

Apply Proposition pfr-rho on \(U_A,U_A\) to get a subspace such that \(2\rho(U_H)\le 2\rho(U_A)+8d[U_A;U_A]\). Recall that \(d[U_A;U_A]\le \log K\) as proved in Lemma pfr_aux, and \(\rho(U_A)=0\) by Lemma rho_of_uniform. Therefore \(\rho(U_H)\le 4\log(K)\). The claim then follows from Rho of subgroup.

Lean

Formalized as better_PFR_conjecture_aux0.

Sources
Leanbetter_PFR_conjecture_aux0
Uses 2 · Used by 1
Proof usespfr-rho · Rho of subgroup
Used bypfr-9-aux'

Corollarypfr-9-aux'#

If \(|A+A| \leq K|A|\), then there exist a subgroup \(H\) and a subset \(c\) of \(G\) with \(A \subseteq c + H\), such that \(|c| \leq K^{5} |A|^{1/2}/|H|^{1/2}\) and \(|H|/|A|\in[K^{-8},K^8]\).

Proof

Apply Corollary pfr-9-aux and Ruzsa covering lemma to get the result, as in the proof of Lemma pfr_aux.

Lean

Formalized as better_PFR_conjecture_aux.

Sources
Leanbetter_PFR_conjecture_aux
Uses 2 · Used by 3
Proof usespfr-9-aux · Ruzsa covering lemma
Used byApproximate homomorphism form of PFR · PFR with \(C=9\) · Homomorphism form of PFR

TheoremPFR with \(C=9\)#

If \(A \subset {\bf F}_2^n\) is finite non-empty with \(|A+A| \leq K|A|\), then there exists a subgroup \(H\) of \({\bf F}_2^n\) with \(|H| \leq |A|\) such that \(A\) can be covered by at most \(2K^9\) translates of \(H\).

Proof

Given Corollary pfr-9-aux', the proof is the same as that of PFR.

Lean

Formalized as better_PFR_conjecture.

Sources
Leanbetter_PFR_conjecture
Uses 2
Proof usespfr-9-aux' · Ruzsa covering lemma

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.