Improving the exponents

The arguments here are due to Jyun-Jie Liao.

Previously in Definition eta-def we had set \(\eta=1/9\). To implement this chapter, one should refactor the previous arguments so that \(\eta\) is now free to be a positive number, though the specific hypothesis \(\eta=1/9\) would now need to be added to \(\tau\)-decrement.

Let \(X^0_1, X^0_2\) be \(G\)-valued random variables, and let \(X_1, X_2\) be \(\tau\)-minimizers as defined in \(\tau\)-minimizer.

For the next two lemmas, let \((T_1,T_2,T_3)\) be a \(G^3\)-valued random variable such that \(T_1+T_2+T_3=0\) holds identically. Let \(\delta\) be the quantity in (1).

We have the following variant of Constructing good variables, I:

LemmaConstructing good variables, I'#

One has

\[ \begin{aligned} k \leq \delta + \eta (& d[X^0_1;T_1|T_3]-d[X^0_1;X_1]) + \eta (d[X^0_2;T_2|T_3]-d[X^0_2;X_2]). \end{aligned} \]
Proof

We apply Balog-Szemerédi-Gowers with \((A,B) = (T_1, T_2)\) there. Since \(T_1 + T_2 = T_3\), the conclusion is that

\[ \begin{aligned} \sum_{t_3} \mathbb{P}[T_3 = t_3] & d[(T_1 | T_3 = t_3); (T_2 | T_3 = t_3)] \\ & \leq 3 \mathbb{I}[T_1 : T_2] + 2 \mathbb{H}[T_3] - \mathbb{H}[T_1] - \mathbb{H}[T_2].\qquad\text{(1)}\end{aligned} \]

The right-hand side in (1) can be rearranged as

\[ \begin{aligned} & 2( \mathbb{H}[T_1] + \mathbb{H}[T_2] + \mathbb{H}[T_3]) - 3 \mathbb{H}[T_1,T_2] \\ & = 2(\mathbb{H}[T_1] + \mathbb{H}[T_2] + \mathbb{H}[T_3]) - \mathbb{H}[T_1,T_2] - \mathbb{H}[T_2,T_3] - \mathbb{H}[T_1, T_3] = \delta,\end{aligned} \]

using the fact (from Entropy and relabeling) that all three terms \(\mathbb{H}[T_i,T_j]\) are equal to \(\mathbb{H}[T_1,T_2,T_3]\) and hence to each other. We also have

\[ \begin{aligned} & \sum_{t_3} P[T_3 = t_3] \bigl(d[X^0_1; (T_1 | T_3=t_3)] - d[X^0_1;X_1]\bigr) \\ &\quad = d[X^0_1; T_1 | T_3] - d[X^0_1;X_1] \end{aligned} \]

and similarly

\[ \begin{aligned} & \sum_{t_3} \mathbb{P}[T_3 = t_3] (d[X^0_2;(T_2 | T_3=t_3)] - d[X^0_2; X_2]) \\ &\quad\quad\quad\quad\quad\quad \leq d[X^0_2;T_2|T_3] - d[X^0_2;X_2]. \end{aligned} \]

Putting the above observations together, we have

\[ \begin{aligned} \sum_{t_3} \mathbb{P}[T_3=t_3] \psi[(T_1 | T_3=t_3); (T_2 | T_3=t_3)] \leq \delta + \eta (d[X^0_1;T_1|T_3]-d[X^0_1;X_1]) \\ + \eta (d[X^0_2;T_2|T_3]-d[X^0_2;X_2]) \end{aligned} \]

where we introduce the notation

\[ \psi[Y_1; Y_2] := d[Y_1;Y_2] + \eta (d[X_1^0;Y_1] - d[X_1^0;X_1]) + \eta(d[X_2^0;Y_2] - d[X_2^0;X_2]). \]

On the other hand, from Distance lower bound we have \(k \leq \psi[Y_1;Y_2]\), and the claim follows.

Lean

Formalized as construct_good_prelim'.

Sources
Leanconstruct_good_prelim'
Uses 2 · Used by 1
Proof usesBalog-Szemerédi-Gowers · Distance lower bound
Used byConstructing good variables, II'

(One could in fact refactor Constructing good variables, I to follow from Constructing good variables, I' and Upper bound on conditioned Ruzsa distance).

LemmaConstructing good variables, II'#

One has

\[ \begin{aligned} k & \leq \delta + \frac{\eta}{6} \sum_{i=1}^2 \sum_{1 \leq j,l \leq 3; j \neq l} (d[X^0_i;T_j|T_l] - d[X^0_i; X_i]) \end{aligned} \]
Proof

Average Constructing good variables, I' over all six permutations of \(T_1,T_2,T_3\).

Lean

Formalized as construct_good_improved'.

Sources
Leanconstruct_good_improved'
Uses 1 · Used by 1
Proof usesConstructing good variables, I'
Used byConstructing good variables, III'

Now let \(X_1, X_2, \tilde X_1, \tilde X_2\) be independent copies of \(X_1, X_2, X_1, X_2\), and set

\[ U := X_1 + X_2, \qquad V := \tilde X_1 + X_2, \qquad W := X_1 + \tilde X_1 \]

and

\[ S := X_1 + X_2 + \tilde X_1 + \tilde X_2 \]

and introduce the quantities

\[ k = d[X_1;X_2] \]

and

\[ I_1 = I(U : V \, | \, S). \]

LemmaConstructing good variables, III'#

One has

\[ \begin{aligned} k & \leq I(U : V \, | \, S) + I(V : W \, | \,S) + I(W : U \, | \, S) + \frac{\eta}{6} \sum_{i=1}^2 \sum_{A,B \in \{U,V,W\}: A \neq B} (d[X^0_i;A|B,S] - d[X^0_i; X_i]). \end{aligned} \]
Proof

For each \(s\) in the range of \(S\), apply Constructing good variables, II' with \(T_1,T_2,T_3\) equal to \((U|S=s)\), \((V|S=s)\), \((W|S=s)\) respectively (which works thanks to Key identity), multiply by \(\mathbb{P}[S=s]\), and sum in \(s\) to conclude.

Lean

Formalized as averaged_construct_good.

Sources
Leanaveraged_construct_good
Uses 2 · Used by 1
Proof usesConstructing good variables, II' · Key identity
Used byImproved \(\tau\)-decrement

To control the expressions in the right-hand side of this lemma we need a general entropy inequality.

LemmaGeneral inequality#

Let \(X_1, X_2, X_3, X_4\) be independent \(G\)-valued random variables, and let \(Y\) be another \(G\)-valued random variable. Set \(S := X_1+X_2+X_3+X_4\). Then

\[ \begin{aligned} & d[Y; X_1+X_2|X_1 + X_3, S] - d[Y; X_1] \\ &\quad \leq \tfrac{1}{4} (d[X_1;X_2] + 2d[X_1;X_3] + d[X_2;X_4])\\ &\qquad \qquad + \tfrac{1}{4} (d[X_1|X_1+X_3;X_2|X_2+X_4] - d[X_3|X_3+X_4; X_1|X_1+X_2])\\ &\qquad \qquad + \tfrac{1}{8} (\mathbb{H}[X_1+X_2] - \mathbb{H}[X_3+X_4] + \mathbb{H}[X_2] - \mathbb{H}[X_3]\\ &\qquad \qquad \qquad + \mathbb{H}[X_2|X_2+X_4] - \mathbb{H}[X_1|X_1+X_3]). \end{aligned} \]
Proof

On the one hand, by Upper bound on conditioned Ruzsa distance and two applications of Comparison of Ruzsa distances, I we have

\[ \begin{aligned} &d[Y;X_1+X_2|X_1 + X_3, S] \\ &\quad \leq d[Y;X_1+X_2|S] + \tfrac{1}{2} \mathbb{I}[X_1 + X_2 : X_1 + X_3|S] \\ &\quad \leq d[Y;X_1+X_2]\\ &\qquad + \tfrac{1}{2} (d[X_1+X_2;X_3+X_4] + \mathbb{I}[X_1 + X_2 : X_1 + X_3|S])\\ &\qquad + \tfrac{1}{4} (\mathbb{H}[X_1+X_2] - \mathbb{H}[X_3+X_4])\\ &\quad \leq d[Y;X_1] \\ &\qquad + \tfrac{1}{2} (d[X_1;X_2] + d[X_1+X_2;X_3+X_4] + \mathbb{I}[X_1 + X_2 : X_1 + X_3|S])\\ &\qquad + \tfrac{1}{4} (\mathbb{H}[X_1+X_2] - \mathbb{H}[X_3+X_4] + \mathbb{H}[X_2] - \mathbb{H}[X_1]). \end{aligned} \]

From Specific fibring identity (with \(Y_1,Y_2,Y_3,Y_4\) set equal to \(X_3, X_1, X_4, X_2\) respectively) one has

\[ d[X_3+X_4; X_1+X_2] + d[X_3|X_3+X_4; X_1|X_1+X_2] \]
\[ + \mathbb{I}[X_3 + X_1 : X_1 + X_2|S] = d[X_3;X_1] + d[X_4;X_2]. \]

Rearranging the mutual information and Ruzsa distances slightly, we conclude that

\[ \begin{aligned} &d[Y;X_1+X_2|X_1 + X_3, S] \\ &\quad \leq d[Y;X_1] \\ &\qquad + \tfrac{1}{2} (d[X_1;X_2] + d[X_1;X_3] + d[X_2;X_4] - d[X_3|X_3+X_4; X_1|X_1+X_2])\\ &\qquad + \tfrac{1}{4} (\mathbb{H}[X_1+X_2] - \mathbb{H}[X_3+X_4] + \mathbb{H}[X_2] - \mathbb{H}[X_1]). \end{aligned} \]

On the other hand, \((X_1+X_2|X_1 + X_3, S)\) has an identical distribution to the independent sum of \((X_1|X_1+X_3)\) and \((X_2|X_2+X_4)\). We may therefore apply Comparison of Ruzsa distances, I to conditioned variables \((X_1|X_1+X_3=s)\) and \((X_2|X_2+X_4=t)\) and average in \(s,t\) to obtain the alternative bound

\[ \begin{aligned} & d[Y;X_1+X_2|X_1 + X_3, S] \\ &\quad \leq d[Y;X_1|X_1+X_3] + \tfrac{1}{2} d[X_1|X_1+X_3; X_2|X_2+X_4] \\ &\qquad + \tfrac{1}{4} (\mathbb{H}[X_2|X_2+X_4] - \mathbb{H}[X_1|X_1+X_3]) \\ &\quad \leq d[Y;X_1] \\ &\qquad + \tfrac{1}{2} (d[X_1;X_3] + d[X_1|X_1+X_3;X_2|X_2+X_4])\\ &\qquad + \tfrac{1}{4} (\mathbb{H}[X_2|X_2+X_4] - \mathbb{H}[X_1|X_1+X_3] + \mathbb{H}[X_1] - \mathbb{H}[X_3]). \end{aligned} \]

If one takes the arithmetic mean of these two bounds and simplifies using Specific fibring identity, one obtains the claim.

Lean

Formalized as gen_ineq_00, gen_ineq_01, gen_ineq_10.

Sources
Leangen_ineq_00 · gen_ineq_01 · gen_ineq_10
Uses 3 · Used by 1
Proof usesUpper bound on conditioned Ruzsa distance · Comparison of Ruzsa distances, I · Specific fibring identity
Used byBound on distance differences

Returning to our specific situation, we now have

LemmaBound on distance differences#

We have

\[ \begin{aligned} &\sum_{i=1}^2 \sum_{A,B \in \{U,V,W\}: A \neq B} d[X_i^0;A|B, S] - d[X_i^0;X_i]\\ &\qquad \leq 12 k + \frac{4(2 \eta k - I_1)}{1-\eta}. \end{aligned} \]
Proof

If we apply General inequality with \(X_1:=X_1\), \(Y:=X_1^0\) and \((X_2,X_3,X_4)\) equal to the \(3!\) permutations of \((X_2,\tilde X_1,\tilde X_2)\), and sums (using the symmetry \(\mathbb{H}[X|X+Y] = \mathbb{H}[Y|X+Y]\), which follows from Conditional entropy and relabeling), we can bound

\[ \sum_{A,B \in \{U,V,W\}: A \neq B} d[X_1^0;A|B, S] - d[X_1^0;X_1] \]

by

\[ \begin{aligned} &\quad \tfrac{1}{4} (6d[X_1;X_2] + 6d[X_1;\tilde X_2]\\ &\qquad + 6d[X_1;\tilde X_1] + 2d[\tilde X_1;\tilde X_2] + 2 d[\tilde X_1;X_2] + 2d[X_2;\tilde X_2])\\ &\quad + \tfrac{1}{8} (2\mathbb{H}[X_1+X_2] + 2\mathbb{H}[X_1+\tilde X_1] + 2 \mathbb{H}[X_1+\tilde X_2] \\ &\qquad - 2\mathbb{H}[\tilde X_1+X_2] - 2\mathbb{H}[X_2+\tilde X_2] - 2\mathbb{H}[\tilde X_1+\tilde X_2])\\ &\qquad \qquad + \tfrac{1}{4} (\mathbb{H}[X_2|X_2+\tilde X_2] + \mathbb{H}[\tilde X_1|\tilde X_1+\tilde X_2] + \mathbb{H}[\tilde X_1|X_1+\tilde X_2] \\ &\qquad \qquad \qquad - \mathbb{H}[X_1|X_1+\tilde X_1] - \mathbb{H}[X_1|X_1+X_2] - \mathbb{H}[X_1|X_1+\tilde X_2]), \end{aligned} \]

which simplifies to

\[ \begin{aligned} &\quad \tfrac{1}{4} (16k + 6d[X_1;X_1] + 2d[X_2;X_2])\\ &\qquad \qquad + \tfrac{1}{4} (H[X_1+\tilde X_1] - H[X_2+\tilde X_2] + d[X_2|X_2+\tilde X_2] - d[X_1|X_1+\tilde X_1]). \end{aligned} \]

A symmetric argument also bounds

\[ \sum_{A,B \in \{U,V,W\}: A \neq B} d[X_2^0;A|B, S] - d[X_2^0;X_2] \]

by

\[ \begin{aligned} &\quad \tfrac{1}{4} (16k + 6d[X_2;X_2] + 2d[X_1;X_1])\\ &\qquad \qquad + \tfrac{1}{4} (H[X_2+\tilde X_2] - H[X_1+\tilde X_1] + d[X_1|X_1+\tilde X_1] - d[X_2|X_2+\tilde X_2]). \end{aligned} \]

On the other hand, from Lemma second-estimate-aux one has

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

Summing the previous three estimates, we obtain the claim.

Lean

Formalized as dist_diff_bound_1, dist_diff_bound_2.

Sources
Leandist_diff_bound_1 · dist_diff_bound_2
Uses 3 · Used by 1
Proof usesGeneral inequality · Conditional entropy and relabeling · second-estimate-aux
Used byImproved \(\tau\)-decrement

TheoremImproved \(\tau\)-decrement#

Suppose \(0 < \eta < 1/8\). Let \(X_1, X_2\) be tau-minimizers. Then \(d[X_1;X_2] = 0\).

Proof

From Constructing good variables, III', Bound on distance differences, and Bound on conditional mutual informations one has

\[ k \leq 8\eta k - \frac{(1 -5 \eta - \frac{4}{6} \eta)(2 \eta k - I_1)}{(1-\eta)}. \]

For any \(\eta < 1/8\), we see from First estimate that the expression \(\frac{(1 -5 \eta - \frac{4}{6} \eta)(2 \eta k - I_1)}{(1-\eta)}\) is nonnegative, and hence \(k = 0\) as required.

Lean

Formalized as tau_strictly_decreases'.

Sources
Leantau_strictly_decreases'
Uses 3 · Used by 1
Proof usesConstructing good variables, III' · Bound on distance differences · Bound on conditional mutual informations
Used byLimiting improved \(\tau\)-decrement

TheoremLimiting improved \(\tau\)-decrement#

For \(\eta = 1/8\), there exist tau-minimizers \(X_1, X_2\) satisfying \(d[X_1;X_2] = 0\).

Proof

For each \(\eta<1/8\), consider minimizers \(X_1^\eta\) and \(X_2^\eta\) from \(\tau\) has minimum. By Improved \(\tau\)-decrement, they satisfy \(d[X_1^\eta; X_2^\eta]=0\). By compactness of the space of probability measures on \(G\), one may extract a converging subsequence of the distributions of \(X_1^\eta\) and \(X_2^\eta\) as \(\eta \to 1/8\). By continuity of all the involved quantities, the limit is a pair of tau-minimizers for \(1/8\) satisfying additionally \(d[X_1;X_2] = 0\).

Lean

Formalized as tau_minimizer_exists_rdist_eq_zero.

Sources
Leantau_minimizer_exists_rdist_eq_zero
Uses 2 · Used by 1
Proof usesImproved \(\tau\)-decrement · \(\tau\) has minimum
Used byImproved entropy version of PFR

TheoremImproved entropy version of PFR#

Let \(G = \mathbb{F}_2^n\), and suppose that \(X^0_1, X^0_2\) are \(G\)-valued random variables. Then there is some subgroup \(H \leq G\) such that

\[ d[X^0_1;U_H] + d[X^0_2;U_H] \le 10 d[X^0_1;X^0_2], \]

where \(U_H\) is uniformly distributed on \(H\). Furthermore, both \(d[X^0_1;U_H]\) and \(d[X^0_2;U_H]\) are at most \(\tfrac{11}{2} d[X^0_1;X^0_2]\).

Proof

Let \(X_1, X_2\) be the good \(\tau\)-minimizer from Limiting improved \(\tau\)-decrement. By construction, \(d[X_1;X_2]=0\). From General 100% inverse theorem, \(d[X_1;U_H] = d[X_2; U_H] = 0\). Also from \(\tau\)-minimization we have \(\tau[X_1;X_2] \leq \tau[X^0_2;X^0_1]\). Using this and the Ruzsa triangle inequality we can conclude.

Lean

Formalized as entropic_PFR_conjecture_improv.

Sources
Leanentropic_PFR_conjecture_improv
Uses 3 · Used by 2
Proof usesLimiting improved \(\tau\)-decrement · General 100% inverse theorem · Ruzsa triangle inequality
Used bypfr_aux-improv · app-ent-pfr

One can then replace Lemma pfr_aux with

Lemmapfr_aux-improv#

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^6 |A|^{1/2}/|H|^{1/2}\) translates of a subspace \(H\) of \({\bf F}_2^n\) with

\[ |H|/|A| \in [K^{-10}, K^{10}]. \]
Proof

By repeating the proof of Lemma pfr_aux and using Improved entropy version of PFR one can obtain the claim with \(13/2\) replaced with \(6\) and \(11\) replaced by \(10\).

Lean

Formalized as PFR_conjecture_improv_aux.

Sources
LeanPFR_conjecture_improv_aux
Uses 8 · Used by 1
Proof usesImproved entropy 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 byImproved PFR

This implies the following improved version of Theorem PFR:

TheoremImproved PFR#

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

Proof

By repeating the proof of PFR and using Lemma pfr_aux-improv one obtains \(2K^{11}\) in place of \(2K^{12}\).

Lean

Formalized as PFR_conjecture_improv.

Sources
LeanPFR_conjecture_improv
Uses 1
Proof usespfr_aux-improv

Of course, by replacing PFR with Improved PFR we may also improve constants in downstream theorems in a straightforward manner.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.