Endgame

Let \(X_1,X_2,\tilde X_1,\tilde X_2\) be as before, and introduce the random variables

\[ 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. \]

LemmaSymmetry identity#

We have

\[ I(U:W | S) = I(V:W | S). \]
Proof

This should follow from Copy preserves entropy, Alternate formula for conditional mutual information, and Chain rule.

Lean

Formalized as I₃_eq.

Sources
LeanI₃_eq
Uses 3 · Used by 1
Proof usesCopy preserves entropy · Alternate formula for conditional mutual information · Chain rule
Used byBound on conditional mutual informations

LemmaBound on conditional mutual informations#

We have

\[ I(U : V \, | \, S) + I(V : W \, | \,S) + I(W : U \, | \, S) \leq 6 \eta k - \frac{1 - 5 \eta}{1-\eta} (2 \eta k - I_1). \]
Proof

From the definitions of \(I_1,I_2\) and Symmetry identity, we see that

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

Applying First estimate and Second estimate we have the inequalities

\[ I_2 \leq 2 \eta k + \frac{2\eta(2 \eta k - I_1)}{1-\eta} . \]

We conclude that

\[ I_1 + I_2 + I_2 \leq I_1+4\eta k+ \frac{4\eta(2 \eta k - I_1)}{1-\eta} \]

and the claim follows from some calculation.

Lean

Formalized as I₃_eq, sum_condMutual_le.

Sources
LeanI₃_eq · sum_condMutual_le
Uses 3 · Used by 2
Statement usesConditional mutual information
Proof usesSecond estimate · Symmetry identity
Used by\(\tau\)-decrement · Improved \(\tau\)-decrement

LemmaBound on distance increments#

We have

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

By Comparison of Ruzsa distances, II (taking \(X = X_1^0\), \(Y = X_1\), \(Z = X_2\) and \(Z' = \tilde X_1 + \tilde X_2\), so that \(Y + Z = U\) and \(Y + Z + Z' = S\)) we have, noting that \(\mathbb{H}[Y+ Z] = \mathbb{H}[Z']\),

\[ d[X^0_1;U|S] - d[X^0_1;X_1] \leq \tfrac{1}{2} (\mathbb{H}[S] - \mathbb{H}[X_1]). \]

Further applications of Comparison of Ruzsa distances, II give

\[ \begin{aligned} d[X^0_2;U|S] - d[X^0_2; X_2] &\leq \tfrac{1}{2} (\mathbb{H}[S] - \mathbb{H}[X_2]) \\ d[X^0_1;V|S] - d[X^0_1;X_1] &\leq \tfrac{1}{2} (\mathbb{H}[S] - \mathbb{H}[X_1])\\ d[X^0_2;V|S] - d[X^0_2;X_2] &\leq \tfrac{1}{2} (\mathbb{H}[S] - \mathbb{H}[X_2]) \end{aligned} \]

and

\[ d[X^0_1;W|S] - d[X^0_1;X_1] \leq \tfrac{1}{2} (\mathbb{H}[S] + \mathbb{H}[W] - \mathbb{H}[X_1] - \mathbb{H}[W']), \]

where \(W' := X_2 + \tilde X_2\). To treat \(d[X^0_2;W|S]\), first note that this equals \(d[X^0_2;W'|S]\), since for a fixed choice \(s\) of \(S\) we have \(W' = W + s\) (here we need some helper lemma about Ruzsa distance). Now we may apply Comparison of Ruzsa distances, II to obtain

\[ d[X^0_2;W'|S] - d[X^0_2;X_2] \leq \tfrac{1}{2} (\mathbb{H}[S] + \mathbb{H}[W'] - \mathbb{H}[X_2] - \mathbb{H}[W]). \]

Summing these six estimates and using Entropy bound on quadruple sum, we conclude that

\[ \begin{aligned} \sum_{i=1}^2 \sum_{A\in\{U,V,W\}} \big(d[X^0_i;A|S] & - d[X^0_i;X_i]\big) \\ &\leq 3 \mathbb{H}[S] - \tfrac{3}{2} \mathbb{H}[X_1] - \tfrac{3}{2} \mathbb{H}[X_2]\\ &\leq (6 - 3\eta) k + 3(2 \eta k - I_1) \end{aligned} \]

as required.

Lean

Formalized as sum_dist_diff_le.

Sources
Leansum_dist_diff_le
Uses 2 · Used by 1
Proof usesComparison of Ruzsa distances, II · Entropy bound on quadruple sum
Used by\(\tau\)-decrement

LemmaKey identity#

We have \(U+V+W=0\).

Proof

Obvious because we are in characteristic two.

Lean

Formalized as sum_uvw_eq_zero.

Sources
Leansum_uvw_eq_zero
Used by 2
Used by\(\tau\)-decrement · Constructing good variables, III'

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. Set

\[ \delta := \sum_{1 \leq i < j \leq 3} \mathbb{I}[T_i;T_j].\qquad\text{(1)} \]

LemmaConstructing good variables, I#

One has

\[ \begin{aligned} k \leq \delta + \eta (& d[X^0_1;T_1]-d[X^0_1;X_1]) + \eta (d[X^0_2;T_2]-d[X^0_2;X_2]) \\ & + \tfrac12 \eta \mathbb{I}[T_1:T_3] + \tfrac12 \eta \mathbb{I}[T_2:T_3]. \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{(2)}\end{aligned} \]

The right-hand side in (2) 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] \leq d[X^0_1;T_1] - d[X^0_1;X_1] + \tfrac{1}{2} \mathbb{I}[T_1 : T_3] \end{aligned} \]

by Upper bound on conditioned Ruzsa distance, 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] - d[X^0_2;X_2] + \tfrac{1}{2} \mathbb{I}[T_2 : T_3]. \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]-d[X^0_1;X_1]) \\ + \eta (d[X^0_2;T_2]-d[X^0_2;X_2]) + \tfrac12 \eta \mathbb{I}[T_1:T_3] + \tfrac12 \eta \mathbb{I}[T_2:T_3] \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 3 · Used by 1
Proof usesBalog-Szemerédi-Gowers · Upper bound on conditioned Ruzsa distance · Distance lower bound
Used byConstructing good variables, II

(Note: in the paper, this lemma was phrased in a more intuitive formulation that is basically the contrapositive of the one here. Similarly for the next two lemmas.)

The proof of Constructing good variables, I is shown with its statement.

LemmaConstructing good variables, II#

One has

\[ \begin{aligned} k & \leq \delta + \frac{\eta}{3} \biggl( \delta + \sum_{i=1}^2 \sum_{j = 1}^3 (d[X^0_i;T_j] - d[X^0_i; X_i]) \biggr). \end{aligned} \]
Proof

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

Lean

Formalized as construct_good.

Sources
Leanconstruct_good
Uses 1 · Used by 1
Proof usesConstructing good variables, I
Used by\(\tau\)-decrement

Theorem\(\tau\)-decrement#

Let \(X_1, X_2\) be tau-minimizers. Then \(d[X_1;X_2] = 0\).

Proof

Set \(k := d[X_1;X_2]\). Applying Constructing good variables, II with any random variables \((T_1,T_2,T_3)\) such that \(T_1+T_2+T_3=0\) holds identically, we deduce that

\[ k \leq \delta + \frac{\eta}{3} \biggl( \delta + \sum_{i=1}^2 \sum_{j = 1}^3 (d[X^0_1;T_j] - d[X^0_i;X_i]) \biggr). \]

Note that \(\delta\) is still defined by (1) and thus depends on \(T_1,T_2,T_3\). In particular we may apply this for

\[ T_1 = (U | S = s),\qquad T_2 = (V | S = s), \qquad T_3 = (W | S = s) \]

for \(s\) in the range of \(S\) (which is a valid choice by Key identity) and then average over \(s\) with weights \(p_S(s)\), to obtain

\[ k \leq \tilde \delta + \frac{\eta}{3} \biggl( \tilde \delta + \sum_{i=1}^2 \sum_{A\in\{U,V,W\}} \bigl( d[X^0_i;A|S] - d[X^0_i;X_i]\bigr) \biggr), \]

where

\[ \tilde \delta := \mathbb{I}[U : V | S] + \mathbb{I}[V : W | S] + \mathbb{I}[W : U | S]. \]

Putting this together with Bound on conditional mutual informations and Bound on distance increments, we conclude that

\[ \begin{aligned} k &\leq \Bigl(1+\frac{\eta}{3}\Bigr)\Bigl(6\eta k-\frac{1-5\eta}{1-\eta}(2\eta k-I_1)\Bigr)+\frac{\eta}{3}\Bigl((6-3\eta)k+3(2\eta k-I_1)\Bigr)\\ &= (8\eta + \eta^2) k - \biggl( \frac{1 - 5 \eta}{1-\eta}\Bigl(1 + \frac{\eta}{3}\Bigr) - \eta \biggr)(2 \eta k - I_1)\\ &\leq (8 \eta + \eta^2) k \end{aligned} \]

since the quantity \(2 \eta k - I_1\) is non-negative (by First estimate), and its coefficient in the above expression is non-positive provided that \(\eta(2\eta + 17) \le 3\), which is certainly the case with Definition eta-def. Moreover, from Definition eta-def we have \(8 \eta + \eta^2 < 1\). It follows that \(k=0\), as desired.

Lean

Formalized as tau_strictly_decreases.

Sources
Leantau_strictly_decreases
Uses 5 · Used by 1
Proof usesConstructing good variables, II · Key identity · Bound on conditional mutual informations · Bound on distance increments · First estimate
Used byEntropy version of PFR

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.