Endgame
Now let \(m \geq 2\), let \(G\) be an \(m\)-torsion abelian group, and let \((X_i)_{1 \leq i \leq m}\) be a \(\tau\)-minimizer.
LemmaZero-sum#
We have
Used by 1
PropositionMutual information bound#
We have
where
Proof
We analyze these variables by Bounding mutual information in several different ways. In the first application, take \(X_{i,j}=Y_{i,j}\). Note that each column \((X_{i,j})_{i=1}^m\) is indeed a permutation of \(X_1,\dots,X_m\); in fact, the trivial permutation. Note also that for each \(i \in \mathbb{Z}/m\mathbb{Z}\), the row sum is
and for each \(j \in \mathbb{Z}/m\mathbb{Z}\), the column sum is
Finally note that \(\sum_{i,j=1}^m X_{i,j} = W\). From Bounding mutual information we then have
with \(t\) as in (2). Since \(Z_1\) is a function of \((P_i)_{i \in \mathbb{Z}/m\mathbb{Z}}\) by Additional random variables, and similarly \(Z_2\) is a function of \((Q_j)_{j \in \mathbb{Z}/m\mathbb{Z}}\), it follows immediately from Data processing inequality that
In the second application of Bounding mutual information, we instead consider \(X'_{i,j} = Y_{i-j,j}\). Again, for each fixed \(j\), the tuple \((X'_{i,j})_{i=1}^m\) is a permutation of \(X_1,\dots,X_m\). This time the row sums for \(i \in \{1,\dots, m\}\) are
Similarly, the column sums for \(j \in \{1,\dots, m\}\) are
As before, \(\sum_{i,j=1}^m X'_{i,j} = W\). Hence, using Additional random variables and Data processing inequality again, Bounding mutual information tells us
In the third application (In fact, by permuting the variables \((Y_{i,j})_{i,j \in \mathbb{Z}/m\mathbb{Z}}\), one can see that the random variables \((W, Z_1, Z_2)\) and \((W, Z_1, Z_3)\) have the same distribution, so this is in some sense identical to – and can be deduced from – the first application.) of Bounding mutual information, take \(X''_{i,j} = Y_{i,j-i}\). The column and row sums are respectively
and
Hence, Bounding mutual information and Data processing inequality give
which completes the proof.
Lean
Formalized as mutual_information_le_t_12, mutual_information_le_t_13, mutual_information_le_t_23.
Sources
Uses 2 · Used by 1
LemmaEntropy of \(W\)#
We have \(\mathbb{H}[W] \leq (2m-1)k + \frac1m \sum_{i=1}^m \mathbb{H}[X_i]\).
Proof
Without loss of generality, we may take \(X_1,\dots,X_m\) to be independent. Write \(S = \sum_{i=1}^m X_i\). Note that for each \(j \in \mathbb{Z}/m\mathbb{Z}\), the sum \(Q_j\) from Additional random variables above has the same distribution as \(S\). By Kaimonovich–Vershik–Madiman inequality we have
By Multidistance and Ruzsa distance, IV, we have
and hence
From Multidistance we have
and the claim follows.
Lean
Formalized as entropy_of_W_le.
Sources
Uses 3 · Used by 1
LemmaEntropy of \(Z_2\)#
We have \(\mathbb{H}[Z_2] \leq (8m^2-16m+1) k + \frac{1}{m} \sum_{i=1}^m \mathbb{H}[X_i]\).
Proof
We observe
Applying Kaimonovich–Vershik–Madiman inequality one has
Using Sums of dilates II and (3) we get
Applying (4) gives the claim.
Lean
Formalized as entropy_of_Z_two_le.
Sources
Uses 2 · Used by 1
LemmaMutual information bound#
We have \(\mathbb{I}[W : Z_2] \leq 2 (m-1) k\).
Proof
From Alternative formulae for mutual information we have \(\mathbb{I}[W : Z_2] = \mathbb{H}[W] - \mathbb{H}[W | Z_2]\), and since \(Z_2 = \sum_{j=1}^{m-1} j Q_j\) and \(W = \sum_{j=1}^m Q_j\),
Hence, by Entropy of \(W\),
as claimed.
Lean
Formalized as mutual_of_W_Z_two_le.
Sources
Uses 2 · Used by 1
LemmaDistance bound#
We have \(\sum_{i=1}^m d[X_i;Z_2|W] \leq 4(m^3-m^2) k\).
Proof
For each \(i \in \{1,\dots, m\}\), using Kaimonovich–Vershik–Madiman inequality, III (noting the sum \(Z_2\) contains \(X_i\) as a summand) we have
and using Upper bound on conditioned Ruzsa distance we have
Combining with (5) and Mutual information bound gives
Summing over \(i\) and applying Entropy of \(Z_2\) gives
Finally, applying Multidistance and Ruzsa distance, II (and dropping some lower order terms) gives the claim.
Lean
Formalized as sum_of_conditional_distance_le.
Sources
Uses 5 · Used by 1
LemmaApplication of BSG#
Let \(G\) be an abelian group, 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, and write
Let \(Y_1,\dots,Y_n\) be some further \(G\)-valued random variables and let \(\alpha>0\) be a constant. Then there exists a random variable \(U\) such that
Proof
We apply Balog-Szemerédi-Gowers with \(X=T_1\) and \(Y=T_2\). Since \(T_1+T_2=-T_3\), we find that
where the last line follows from Entropy and relabeling by observing
since any two of \(T_1,T_2,T_3\) determine the third.
By (7) and the triangle inequality,
and by Comparison of Ruzsa distances, I, for each \(Y_i\),
Hence,
and the result follows by setting \(U=(T_2 \,|\, T_3 \mathop{=} z)\) for some \(z\) such that the quantity in parentheses on the left-hand side is at most the weighted average value.
Lean
Formalized as dist_of_U_add_le.
Sources
Uses 3 · Used by 1
PropositionVanishing entropy#
We have \(k = 0\).
Proof
For each value \(W=w\), apply Application of BSG (and Zero-sum) to
with \(Y_i=X_i\) and \(\alpha=\eta/m\). Write
for this choice, and note that
by Mutual information bound. Write \(U_w\) for the random variable guaranteed to exist by Application of BSG, so that (6) gives
Let \((U_w)_I\) denote the tuple consisting of the same variable \(U_w\) repeated \(m\) times. By Multidistance and Ruzsa distance, III
On the other hand, from Lower bound on multidistance one has
Combining (9), (10) and (11) and averaging over \(w\) (with weight \(p_W(w)\)), and recalling the value \(\alpha=\eta/m\), gives
since the terms \(d[X_i; U_w]\) cancel by our choice of \(\alpha\). Substituting in Distance bound and (8), and using the fact that \(2 + \frac{\eta}{2} < 3\), we have
From \(\eta\) we have we have
and hence \(k \leq 0\). The claim now follows from Nonnegativity.
Lean
Formalized as k_eq_zero.
Sources
Uses 8 · Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.