Kaimanovich-Vershik-Madiman… to Comparison of Ruzsa distances…

LemmaKaimanovich-Vershik-Madiman inequality#

Suppose that \(X, Y, Z\) are independent \(G\)-valued random variables. Then

\[ \mathbb{H}[X + Y + Z] - \mathbb{H}[X + Y] \leq \mathbb{H}[Y+ Z] - \mathbb{H}[Y]. \]
Proof

From Submodularity we have

\[ \mathbb{H}[X, X + Y+ Z] + \mathbb{H}[Z, X + Y+ Z] \geq \mathbb{H}[X, Z, X + Y+ Z] + \mathbb{H}[X + Y+ Z]. \]

However, using Lemmas Additivity of entropy, Entropy and relabeling repeatedly we have \(\mathbb{H}[X, X + Y+ Z] = \mathbb{H}[X, Y+ Z] = \mathbb{H}[X] + \mathbb{H}[Y+ Z]\), \(\mathbb{H}[Z, X + Y + Z] = \mathbb{H}[Z, X + Y] = \mathbb{H}[Z] + \mathbb{H}[X + Y]\) and \(\mathbb{H}[X, Z, X + Y+ Z] = \mathbb{H}[X, Y, Z] = \mathbb{H}[X] + \mathbb{H}[Y] + \mathbb{H}[Z]\). The claim then follows from a calculation.

Lean

Formalized as kaimanovich_vershik.

Sources
Leankaimanovich_vershik
Uses 3 · Used by 6
Proof usesSubmodularity · Additivity of entropy · Entropy and relabeling
Used byComparison of Ruzsa distances, I · Comparing sums · Kaimonovich–Vershik–Madiman inequality · Kaimonovich–Vershik–Madiman inequality, III · Sums of dilates II · Multidistance and Ruzsa distance, IV

LemmaExistence of conditional independent trials#

For \(X,Y\) random variables, there exist random variables \(X_1,X_2,Y'\) on a common probability space with \((X_1, Y'), (X_2, Y')\) both having the distribution of \((X,Y)\), and \(X_1, X_2\) conditionally independent over \(Y'\) in the sense of Conditionally independent random variables.

Proof

Explicit construction.

Lean

Formalized as ProbabilityTheory.condIndep_copies.

Sources
LeanProbabilityTheory.condIndep_copies
Uses 1 · Used by 2
Statement usesConditionally independent random variables
Used byBalog-Szemerédi-Gowers · Flipping a sign

LemmaBalog-Szemerédi-Gowers#

Let \(A,B\) be \(G\)-valued random variables on \(\Omega\), and set \(Z := A+B\). Then

\[ \sum_{z} \mathbb{P}[Z=z] d[(A | Z = z); (B | Z = z)] \leq 3 \mathbb{I}[A:B] + 2 \mathbb{H}[Z] - \mathbb{H}[A] - \mathbb{H}[B].\qquad\text{(2)} \]
Proof

Let \((A_1, B_1)\) and \((A_2, B_2)\) (and \(Z'\), which by abuse of notation we call \(Z\)) be conditionally independent trials of \((A,B)\) relative to \(Z\) as produced by Existence of conditional independent trials, thus \((A_1,B_1)\) and \((A_2,B_2)\) are coupled through the random variable \(A_1 + B_1 = A_2 + B_2\), which by abuse of notation we shall also call \(Z\).

Observe from Ruzsa distance in independent case that the left-hand side of (2) is

\[ \mathbb{H}[A_1 - B_2| Z] - \mathbb{H}[A_1 | Z]/2 - \mathbb{H}[B_2 | Z]/2.\qquad\text{(3)} \]

since, crucially, \((A_1 | Z=z)\) and \((B_2 | Z=z)\) are independent for all \(z\).

Applying submodularity (Alternate form of submodularity) gives

\[ \begin{split} &\mathbb{H}[A_1 - B_2] + \mathbb{H}[A_1 - B_2, A_1, B_1] \\ &\qquad \leq \mathbb{H}[A_1 - B_2, A_1] + \mathbb{H}[A_1 - B_2,B_1]. \end{split}\qquad\text{(4)} \]

We estimate the second, third and fourth terms appearing here. First note that, by Entropy of conditionally independent variables and Entropy and relabeling (noting that the tuple \((A_1 - B_2, A_1, B_1)\) determines the tuple \((A_1, A_2, B_1, B_2)\) since \(A_1+B_1=A_2+B_2\))

\[ \mathbb{H}[A_1 - B_2, A_1, B_1] = \mathbb{H}[A_1, B_1, A_2, B_2,Z] = 2\mathbb{H}[A,B] - \mathbb{H}[Z].\qquad\text{(5)} \]

Next observe that

\[ \mathbb{H}[A_1 - B_2, A_1] = \mathbb{H}[A_1, B_2] \leq \mathbb{H}[A] + \mathbb{H}[B].\qquad\text{(6)} \]

Finally, we have

\[ \mathbb{H}[A_1 - B_2, B_1] = \mathbb{H}[A_2 - B_1, B_1] = \mathbb{H}[A_2, B_1] \leq \mathbb{H}[A] + \mathbb{H}[B].\qquad\text{(7)} \]

Substituting (5), (6) and (7) into (4) yields

\[ \mathbb{H}[A_1 - B_2] \leq 2 \mathbb{I}[A:B] + \mathbb{H}[Z] \]

and so by Conditioning reduces entropy

\[ \mathbb{H}[A_1 - B_2 | Z] \leq 2 \mathbb{I}[A:B] + \mathbb{H}[Z]. \]

Since

\[ \begin{aligned} \mathbb{H}[A_1 | Z] & = \mathbb{H}[A_1, A_1 + B_1] - \mathbb{H}[Z] \\ & = \mathbb{H}[A,B] - \mathbb{H}[Z] \\ & = \mathbb{H}[Z] - \mathbb{I}[A:B] - 2 \mathbb{H}[Z]- \mathbb{H}[A]-\mathbb{H}[B]\end{aligned} \]

and similarly for \(\mathbb{H}[B_2 | Z]\), we see that (3) is bounded by \(3 \mathbb{I}[A:B] + 2\mathbb{H}[Z]-\mathbb{H}[A]-\mathbb{H}[B]\) as claimed.

Lean

Formalized as ent_bsg.

Sources
Leanent_bsg
Uses 8 · Used by 4
Proof usesExistence of conditional independent trials · Entropy of conditionally independent variables · Conditional entropy · Submodularity · Copy preserves entropy · Entropy and relabeling · Additivity of entropy · Ruzsa distance in independent case
Used byConstructing good variables, I · rho-BSG-triplet · Constructing good variables, I' · Application of BSG

LemmaUpper bound on conditioned Ruzsa distance#

Suppose that \((X, Z)\) and \((Y, W)\) are random variables, where \(X, Y\) take values in an abelian group. Then

\[ d[X | Z;Y | W] \leq d[X ; Y] + \tfrac{1}{2} \mathbb{I}[X : Z] + \tfrac{1}{2} \mathbb{I}[Y : W]. \]

In particular,

\[ d[X ;Y | W] \leq d[X ; Y] + \tfrac{1}{2} \mathbb{I}[Y : W]. \]
Proof

Using Alternate form of distance and Existence of independent copies, if \((X',Z'), (Y',W')\) are independent copies of the variables \((X,Z)\), \((Y,W)\), we have

\[ \begin{aligned} d[X | Z; Y | W]&= \mathbb{H}[X'-Y'|Z',W'] - \tfrac{1}{2} \mathbb{H}[X'|Z'] - \tfrac{1}{2}H[Y'|W'] \\ &\le \mathbb{H}[X'-Y']- \tfrac{1}{2} \mathbb{H}[X'|Z'] - \tfrac{1}{2}H[Y'|W'] \\ &= d[X';Y'] + \tfrac{1}{2} \mathbb{I}[X' : Z'] + \tfrac{1}{2} \mathbb{I}[Y' : W']. \end{aligned} \]

Here, in the middle step we used Conditioning reduces entropy, and in the last step we used Ruzsa distance and Mutual information.

Lean

Formalized as condRuzsaDist_le, condRuzsaDist_le'.

Sources
LeancondRuzsaDist_le · condRuzsaDist_le'
Uses 5 · Used by 4
Statement usesConditioned Ruzsa distance · Mutual information
Proof usesAlternate form of distance · Existence of independent copies · Conditioning reduces entropy
Used byComparison of Ruzsa distances, I · Constructing good variables, I · General inequality · Distance bound

LemmaComparison of Ruzsa distances, I#

Let \(X, Y, Z\) be random variables taking values in some abelian group of characteristic \(2\), and with \(Y, Z\) independent. Then we have

\[ \begin{aligned} d[X ; Y + Z] -d[X ; Y] & \leq \tfrac{1}{2} (\mathbb{H}[Y+ Z] - \mathbb{H}[Y]) \\ & = \tfrac{1}{2} d[Y; Z] + \tfrac{1}{4} \mathbb{H}[Z] - \tfrac{1}{4} \mathbb{H}[Y].\qquad\text{(8)}\end{aligned} \]

and

\[ \begin{aligned} d[X ;Y|Y+ Z] - d[X ;Y] & \leq \tfrac{1}{2} \bigl(\mathbb{H}[Y+ Z] - \mathbb{H}[Z]\bigr) \\ & = \tfrac{1}{2} d[Y;Z] + \tfrac{1}{4} \mathbb{H}[Y] - \tfrac{1}{4} \mathbb{H}[Z].\qquad\text{(9)}\end{aligned} \]
Proof

We first prove (8). We may assume (taking an independent copy, using Existence of independent copies and Copy preserves Ruzsa distance, Ruzsa distance in independent case) that \(X\) is independent of \(Y, Z\). Then we have

\[ \begin{aligned} d[X ;Y+ Z] & - d[X ;Y] \\ & = \mathbb{H}[X + Y + Z] - \mathbb{H}[X + Y] - \tfrac{1}{2}\mathbb{H}[Y + Z] + \tfrac{1}{2} \mathbb{H}[Y].\end{aligned} \]

Combining this with Kaimanovich-Vershik-Madiman inequality gives the required bound. The second form of the result is immediate Ruzsa distance in independent case.

Turning to (9), we have from Mutual information and Entropy and relabeling

\[ \begin{aligned} \mathbb{I}[Y : Y+ Z] & = \mathbb{H}[Y] + \mathbb{H}[Y + Z] - \mathbb{H}[Y, Y + Z] \\ & = \mathbb{H}[Y] + \mathbb{H}[Y + Z] - \mathbb{H}[Y, Z] = \mathbb{H}[Y + Z] - \mathbb{H}[Z],\end{aligned} \]

and so (9) is a consequence of Upper bound on conditioned Ruzsa distance. Once again the second form of the result is immediate from Ruzsa distance in independent case.

Lean

Formalized as condRuzsaDist_diff_le, condRuzsaDist_diff_le', condRuzsaDist_diff_le'''.

Sources
LeancondRuzsaDist_diff_le · condRuzsaDist_diff_le' · condRuzsaDist_diff_le'' · condRuzsaDist_diff_le'''
Uses 6 · Used by 7
Proof usesCopy preserves Ruzsa distance · Existence of independent copies · Kaimanovich-Vershik-Madiman inequality · Ruzsa distance in independent case · Entropy and relabeling · Upper bound on conditioned Ruzsa distance
Used byComparison of Ruzsa distances, II · Upper bound on distance differences · Distance between sums · Second estimate · General inequality · Bounding mutual information · Application of BSG

LemmaComparison of Ruzsa distances, II#

Let \(X, Y, Z, Z'\) be random variables taking values in some abelian group, and with \(Y, Z, Z'\) independent. Then we have

\[ \begin{aligned} & d[X ;Y + Z | Y + Z + Z'] - d[X ;Y] \\ & \qquad \leq \tfrac{1}{2} ( \mathbb{H}[Y + Z + Z'] + \mathbb{H}[Y + Z] - \mathbb{H}[Y] - \mathbb{H}[Z']).\qquad\text{(10)}\end{aligned} \]
Proof

By Comparison of Ruzsa distances, I (with a change of variables) we have

\[ d[X ; Y + Z | Y + Z + Z'] - d[X ; Y + Z] \leq \tfrac{1}{2}( \mathbb{H}[Y + Z + Z'] - \mathbb{H}[Z']). \]

Adding this to (8) gives the result.

Lean

Formalized as condRuzsaDist_diff_ofsum_le.

Sources
LeancondRuzsaDist_diff_ofsum_le
Uses 1 · Used by 1
Proof usesComparison of Ruzsa distances, I
Used byBound on distance increments

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.