Multidistance

We continue to let \(G\) be an abelian group.

DefinitionMultidistance#

Let \(m\) be a positive integer, and let \(X_{[m]} = (X_i)_{1 \leq i \leq m}\) be an \(m\)-tuple of \(G\)-valued random variables \(X_i\). Then we define

\[ D[X_{[m]}] := \mathbb{H}[\sum_{i=1}^m \tilde X_i] - \frac{1}{m} \sum_{i=1}^m \mathbb{H}[\tilde X_i], \]

where the \(\tilde X_i\) are independent copies of the \(X_i\).

Lean

Formalized as multiDist.

Sources
LeanmultiDist
Used by 14
Used byEntropy of \(W\) · Vanishing · Multidistance of copy · Multidistance of independent variables · Nonnegativity · Relabeling · Multidistance and Ruzsa distance, I · Multidistance and Ruzsa distance, II · Multidistance and Ruzsa distance, III · Multidistance and Ruzsa distance, IV · Multidistance chain rule · Alternate form of conditional multidistance · Conditional multidistance · \(\tau\)-functional

LemmaMultidistance of copy#

If \(X_{[m]} = (X_i)_{1 \leq i \leq m}\) and \(Y_{[m]} = (Y_i)_{1 \leq i \leq m}\) are such that \(X_i\) and \(Y_i\) have the same distribution for each \(i\), then \(D[X_{[m]}] = D[Y_{[m]}]\).

Proof

Clear from Lemma Copy preserves entropy.

Lean

Formalized as multiDist_copy.

Sources
LeanmultiDist_copy
Uses 1 · Used by 2
Proof usesMultidistance
Used byMultidistance and Ruzsa distance, I · Multidistance and Ruzsa distance, III

LemmaMultidistance of independent variables#

If \(X_{[m]} = (X_i)_{1 \leq i \leq m}\) are jointly independent, then \(D[X_{[m]}] = \mathbb{H}[\sum_{i=1}^m X_i] - \frac{1}{m} \sum_{i=1}^m \mathbb{H}[X_i]\).

Proof

Clear from definition.

Lean

Formalized as multiDist_indep.

Sources
LeanmultiDist_indep
Uses 1 · Used by 3
Proof usesMultidistance
Used byMultidistance and Ruzsa distance, I · Multidistance and Ruzsa distance, III · Multidistance and Ruzsa distance, IV

LemmaNonnegativity#

For any such tuple, we have \(D[X_{[m]}] \geq 0\).

Proof

From Independent lower bound on sumset one has

\[ \mathbb{H}[\sum_{i =1}^m \tilde X_i] \geq \mathbb{H}[\tilde X_i] \]

for each \(1 \leq i \leq m\). Averaging over \(i\), we obtain the claim.

Lean

Formalized as multiDist_nonneg.

Sources
LeanmultiDist_nonneg
Uses 2 · Used by 3
Statement usesMultidistance
Proof usesIndependent lower bound on sumset
Used byVanishing entropy · Conditional multidistance nonnegative · Minimizer close to reference variables

LemmaRelabeling#

If \(\phi: \{1,\dots,m\} \to \{1,\dots,m\}\) is a bijection, then \(D[X_{[m]}] = D[(X_{\phi(j)})_{1 \leq j \leq m}]\).

Proof

Trivial.

Lean

Formalized as multiDist_of_perm.

Sources
LeanmultiDist_of_perm
Uses 1 · Used by 2
Statement usesMultidistance
Used byBounding mutual information · Lower bound on conditional multidistance, II

LemmaMultidistance and Ruzsa distance, I#

Let \(m \ge 2\), and let \(X_{[m]}\) be a tuple of \(G\)-valued random variables. Then

\[ \sum_{1 \leq j,k \leq m: j \neq k} d[X_j; -X_k] \leq m(m-1) D[X_{[m]}]. \]
Proof

By Copy preserves Ruzsa distance, Multidistance of copy we may take the \(X_i\) to be jointly independent. From Independent lower bound on sumset, we see that for any distinct \(1 \leq j,k \leq m\), we have

\[ \mathbb{H}[X_j+X_k] \leq \mathbb{H}[\sum_{i=1}^m X_i], \]

and hence by Ruzsa distance in independent case

\[ d[X_j;-X_k] \leq \mathbb{H}[\sum_{i=1}^m X_i] - \frac{1}{2} \mathbb{H}[X_j] - \frac{1}{2} \mathbb{H}[X_k]. \]

Summing this over all pairs \((j,k)\), \(j \neq k\) and using Lemma Multidistance of independent variables, we obtain the claim.

Lean

Formalized as multidist_ruzsa_I.

Sources
Leanmultidist_ruzsa_I
Uses 6 · Used by 2
Statement usesMultidistance
Proof usesCopy preserves Ruzsa distance · Independent lower bound on sumset · Ruzsa distance in independent case · Multidistance of independent variables · Multidistance of copy
Used byVanishing · Multidistance and Ruzsa distance, II

LemmaMultidistance and Ruzsa distance, II#

Let \(m \ge 2\), and let \(X_{[m]}\) be a tuple of \(G\)-valued random variables. Then

\[ \sum_{j=1}^m d[X_j;X_j] \leq 2 m D[X_{[m]}]. \]
Proof

From Ruzsa triangle inequality we have \(d[X_j;X_j] \leq 2 d[X_j;-X_k]\), and applying this to every summand in Multidistance and Ruzsa distance, I, we obtain the claim.

Lean

Formalized as multidist_ruzsa_II.

Sources
Leanmultidist_ruzsa_II
Uses 3 · Used by 2
Statement usesMultidistance
Proof usesRuzsa triangle inequality · Multidistance and Ruzsa distance, I
Used byBounding mutual information · Distance bound

LemmaMultidistance and Ruzsa distance, III#

Let \(m \ge 2\), and let \(X_{[m]}\) be a tuple of \(G\)-valued random variables. If the \(X_i\) all have the same distribution, then \(D[X_{[m]}] \leq m d[X_i;X_i]\) for any \(1 \leq i \leq m\).

Proof

By Copy preserves Ruzsa distance, Multidistance of copy we may take the \(X_i\) to be jointly independent. Let \(X_0\) be a further independent copy of the \(X_i\). From Kaimonovich–Vershik–Madiman inequality, we have

\[ \mathbb{H}[-X_0 + \sum_{i=1}^m X_i] - \mathbb{H}[-X_0] \leq \sum_{i=1}^m \mathbb{H}[X_0 - X_i] - \mathbb{H}[-X_0] \]

and hence by Negation preserves entropy and Ruzsa distance in independent case

\[ \mathbb{H}[-X_0 + \sum_{i=1}^m X_i] - \mathbb{H}[X_0] \leq m d[X_i,X_i]. \]

On the other hand, by Independent lower bound on sumset we have

\[ \mathbb{H}[\sum_{i=1}^m X_i] \leq \mathbb{H}[-X_0 + \sum_{i=1}^m X_i] \]

and the claim follows.

Lean

Formalized as multidist_ruzsa_III.

Sources
Leanmultidist_ruzsa_III
Uses 8 · Used by 2
Statement usesMultidistance
Proof usesKaimonovich–Vershik–Madiman inequality · Negation preserves entropy · Ruzsa distance in independent case · Independent lower bound on sumset · Copy preserves Ruzsa distance · Multidistance of copy · Multidistance of independent variables
Used byVanishing entropy · Minimizer close to reference variables

LemmaMultidistance and Ruzsa distance, IV#

Let \(m \ge 2\), and let \(X_{[m]}\) be a tuple of independent \(G\)-valued random variables. Let \(W := \sum_{i=1}^m X_i\). Then

\[ d[W;-W] \leq 2 D[X_i]. \]
Proof

Take \((X'_i)_{1 \leq i \leq m}\) to be further independent copies of \((X_i)_{1 \leq i \leq m}\) (which exist by Existence of independent copies), and write \(W' := \sum_{i=1}^m X'_i\). Fix any distinct \(a,b \in I\).

From Kaimanovich-Vershik-Madiman inequality one has

\[ \mathbb{H}[W + W'] \leq \mathbb{H}[W] + \mathbb{H}[X_{a} + W'] - \mathbb{H}[X_{a}]\qquad\text{(1)} \]

and also

\[ \mathbb{H}[X_a + W'] \leq \mathbb{H}[X_a + X_b] + \mathbb{H}[W'] - \mathbb{H}[X'_b]. \]

Combining this with (1) and then applying Independent lower bound on sumset we have

\[ \begin{aligned} \mathbb{H}[W + W'] & \leq 2\mathbb{H}[W] + \mathbb{H}[X_a + X_b] - \mathbb{H}[X_a] - \mathbb{H}[X_b] \\ & \leq 3 \mathbb{H}[W] - \mathbb{H}[X_a] - \mathbb{H}[X_b]. \end{aligned} \]

Averaging this over all choices of \((a,b)\) gives \(\mathbb{H}[W] + 2 D[X_{[m]}]\), and the claim follows from Ruzsa distance in independent case.

Lean

Formalized as multidist_ruzsa_IV.

Sources
Leanmultidist_ruzsa_IV
Uses 6 · Used by 1
Statement usesMultidistance
Proof usesExistence of independent copies · Kaimanovich-Vershik-Madiman inequality · Independent lower bound on sumset · Ruzsa distance in independent case · Multidistance of independent variables
Used byEntropy of \(W\)

PropositionVanishing#

If \(D[X_{[m]}]=0\), then for each \(1 \leq i \leq m\) there is a finite subgroup \(H_i \leq G\) such that \(d[X_i; U_{H_i}] = 0\).

Proof

From Multidistance and Ruzsa distance, II and Distance nonnegative we have \(d[X_j; X_j]=0\) for all \(1 \leq j \leq m\). The claim now follows from General 100% inverse theorem.

Lean

Formalized as multidist_eq_zero.

Sources
Leanmultidist_eq_zero
Uses 4 · Used by 1
Statement usesMultidistance
Proof usesMultidistance and Ruzsa distance, I · Distance nonnegative · General 100% inverse theorem
Used byEntropy form of PFR

With more effort one can show that \(H_i\) is independent of \(i\), but we will not need to do so here.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.