More Ruzsa distance estimates
Let \(G\) be an additive group.
LemmaFlipping a sign#
If \(X,Y\) are \(G\)-valued, then
Proof
Without loss of generality (using Copy preserves Ruzsa distance and Existence of independent copies) we may take \(X,Y\) to be independent. By \((X_1,Y_1)\), \((X_2,Y_2)\) be copies of \((X,Y)\) that are conditionally independent over \(X_1-Y_1=X_2-Y_2\) (this exists thanks to Existence of conditional independent trials). By Existence of independent copies, we can also find another copy \((X_3,Y_3)\) of \((X,Y)\) that is independent of \(X_1,Y_1,X_2,Y_2\). From Alternate form of submodularity, one has
From Ruzsa distance in independent case, Negation preserves entropy, Copy preserves Ruzsa distance we have
Since \(X_3+Y_3\) is a function of \(X_3,Y_3\), we see from Entropy and relabeling and Additivity of entropy that
Because \(X_1-Y_1=X_2-Y_2\), we have
and thus by Entropy and relabeling
and hence by Subadditivity
Since \(X_3,Y_2\) are independent, we see from Ruzsa distance in independent case, Copy preserves Ruzsa distance that
Similarly
We conclude that
Finally, from Data processing for a single variable we have
From Additivity of entropy followed by Entropy of conditionally independent variables, we have
and thus by Ruzsa distance in independent case, Copy preserves Ruzsa distance, Entropy and relabeling, Additivity of entropy
Applying all of these estimates, the claim now follows from linear arithmetic.
Lean
Formalized as rdist_of_neg_le.
Sources
Uses 10 · Used by 1
LemmaKaimonovich–Vershik–Madiman inequality#
If \(n \geq 0\) and \(X, Y_1, \dots, Y_n\) are jointly independent \(G\)-valued random variables, then
Proof
This is trivial for \(n=0,1\), while the \(n=2\) case is Kaimanovich-Vershik-Madiman inequality. Now suppose inductively that \(n > 2\), and the claim was already proven for \(n-1\). By a further application of Kaimanovich-Vershik-Madiman inequality one has
By induction hypothesis one has
Summing the two inequalities, we obtain the claim.
Lean
Formalized as kvm_ineq_I.
Sources
Uses 1 · Used by 5
LemmaKaimonovich–Vershik–Madiman inequality, II#
If \(n \geq 1\) and \(X, Y_1, \dots, Y_n\) are jointly independent \(G\)-valued random variables, then
Proof
Applying Kaimonovich–Vershik–Madiman inequality with all the \(Y_i\) replaced by \(-Y_i\), and using Negation preserves entropy and Ruzsa distance in independent case, we obtain after some rearranging
From Independent lower bound on sumset we have
for all \(i\); subtracting \(\mathbb{H}[X]\) and averaging, we conclude that
and thus
From Distance controls entropy difference we have
Since \(0 \leq \frac{n-1}{2n} \leq \frac{1}{2}\), the claim follows.
Lean
Formalized as kvm_ineq_II.
Sources
LemmaKaimonovich–Vershik–Madiman inequality, III#
If \(n \geq 1\) and \(X, Y_1, \dots, Y_n\) are jointly independent \(G\)-valued random variables, then
Proof
From Kaimanovich-Vershik-Madiman inequality one has
The claim then follows from Ruzsa distance in independent case and some elementary algebra.
Lean
Formalized as kvm_ineq_III.
Sources
Uses 2 · Used by 2
LemmaComparing sums#
Let \((X_i)_{1 \leq i \leq m}\) and \((Y_j)_{1 \leq j \leq l}\) be tuples of jointly independent random variables (so the \(X\)'s and \(Y\)'s are also independent of each other), and let \(f: \{1,\dots,l\} \to \{1,\dots,m\}\) be a function, then
Proof
Write \(W := \sum_{i=1}^m X_i\). From Independent lower bound on sumset we have
while from Kaimonovich–Vershik–Madiman inequality one has
From Kaimanovich-Vershik-Madiman inequality one has
The claim now follows from Negation preserves entropy and some elementary algebra.
Lean
Formalized as ent_of_sum_le_ent_of_sum.
Sources
Uses 4 · Used by 1
LemmaSums of dilates I#
Let \(X,Y,X'\) be independent \(G\)-valued random variables, with \(X'\) a copy of \(X\), and let \(a\) be an integer. Then
and
Proof
From Improved Ruzsa triangle inequality we have
which gives the first inequality. Similarly from Improved Ruzsa triangle inequality we have
which (when combined with Negation preserves entropy) gives the second inequality.
Lean
Formalized as ent_sub_nsmul_le, ent_of_sub_smul'.
Sources
Uses 2 · Used by 1
LemmaSums of dilates II#
Let \(X,Y\) be independent \(G\)-valued random variables, and let \(a\) be an integer. Then
Proof
From Kaimanovich-Vershik-Madiman inequality one has
which by Ruzsa distance in independent case gives
and hence by Flipping a sign
From Sums of dilates I we then have
and the claim now follows by an induction on \(|a|\).
Lean
Formalized as ent_sub_zsmul_sub_ent_le.
Sources
Uses 4 · Used by 1
We remark that in the paper [GGMT2024] the variant estimate
is also proven by a similar method. This variant is superior for \(|a| \geq 9\) (or \(|a|=7\)); but we will not need this estimate here.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.