The multidistance chain rule

LemmaMultidistance chain rule #

Let \(\pi \colon G \to H\) be a homomorphism of abelian groups and let \(X_{[m]}\) be a tuple of jointly independent \(G\)-valued random variables. Then \(D[X_{[m]}]\) is equal to

\[ D[ X_{[m]} | \pi(X_{[m]}) ] +D[ \pi(X_{[m]}) ] + \mathbb{I}[ \sum_{i=1}^m X_i : \pi(X_{[m]}) \; \big| \; \pi\bigl(\sum_{i=1}^m X_i\bigr) ]\qquad\text{(1)} \]

where \(\pi(X_{[m]}) := (\pi(X_i))_{1 \leq i \leq m}\).

Proof

For notational brevity during this proof, write \(S := \sum_{i=1}^m X_i\).

From Alternate formula for conditional mutual information and Entropy and relabeling, noting that \(\pi(S)\) is determined both by \(S\) and by \(\pi(X_{[m]})\), we have

\[ \mathbb{I}[S:\pi(X_{[m]})|\pi(S)] = \mathbb{H}[S]+\mathbb{H}[\pi(X_{[m]})]-\mathbb{H}[S,\pi(X_{[m]})]-\mathbb{H}[\pi(S)], \]

and by Chain rule the right-hand side is equal to

\[ \mathbb{H}[S]-\mathbb{H}[S|\pi(X_{[m]})]-\mathbb{H}[\pi(S)]. \]

Therefore,

\[ \mathbb{H}[S]=\mathbb{H}[S|\pi(X_{[m]})]+\mathbb{H}[\pi(S)]+\mathbb{I}[S:\pi(X_{[m]})|\pi(S)].\qquad\text{(2)} \]

From a further application of Chain rule and Entropy and relabeling we have

\[ \mathbb{H}[X_i] = \mathbb{H}[X_i \, | \, \pi(X_i)] + \mathbb{H}[\pi(X_i)]\qquad\text{(3)} \]

for all \(1 \leq i \leq m\). Averaging (3) in \(i\) and subtracting this from (2), we obtain the claim from Multidistance.

Lean

Formalized as multiDist_chainRule.

Sources

Polynomial Freiman-Ruzsa blueprint: chapter/torsion.tex, line 375

LeanmultiDist_chainRule

Uses 4 · Used by 1

Statement usesMultidistance

Proof usesAlternate formula for conditional mutual information · Entropy and relabeling · Chain rule

Used byConditional multidistance chain rule

We will need to iterate the multidistance chain rule, so it is convenient to observe a conditional version of this rule, as follows.

LemmaConditional multidistance chain rule #

Let \(\pi \colon G \to H\) be a homomorphism of abelian groups. Let \(I\) be a finite index set and let \(X_{[m]}\) be a tuple of \(G\)-valued random variables. Let \(Y_{[m]}\) be another tuple of random variables (not necessarily \(G\)-valued). Suppose that the pairs \((X_i, Y_i)\) are jointly independent of one another (but \(X_i\) need not be independent of \(Y_i\)). Then

\[ \begin{aligned} D[ X_{[m]} | Y_{[m]} ] &= D[ X_{[m]} \,|\, \pi(X_{[m]}), Y_{[m]}] + D[ \pi(X_{[m]}) \,|\, Y_{[m]}] \\ &\quad\qquad + \mathbb{I}[ \sum_{i=1}^m X_i : \pi(X_{[m]}) \; \big| \; \pi\bigl(\sum_{i=1}^m X_i \bigr), Y_{[m]} ].\qquad\text{(4)}\end{aligned} \]

Proof

For each \(y_i\) in the support of \(p_{Y_i}\), apply Multidistance chain rule with \(X_i\) replaced by the conditioned random variable \((X_i|Y_i=y_i)\), and the claim (4) follows by averaging (1) in the \(y_i\) using the weights \(p_{Y_i}\).

Lean

Formalized as cond_multiDist_chainRule.

Sources

Polynomial Freiman-Ruzsa blueprint: chapter/torsion.tex, line 405

Leancond_multiDist_chainRule

Uses 1 · Used by 1

Proof usesMultidistance chain rule

Used bymultidist-chain-rule-iter

We can iterate the above lemma as follows.

Lemmamultidist-chain-rule-iter #

Let \(m\) be a positive integer. Suppose one has a sequence

\[ G_m \to G_{m-1} \to \dots \to G_1 \to G_0 = \{0\}\qquad\text{(5)} \]

of homomorphisms between abelian groups \(G_0,\dots,G_m\), and for each \(d=0,\dots,m\), let \(\pi_d : G_m \to G_d\) be the homomorphism from \(G_m\) to \(G_d\) arising from this sequence by composition (so for instance \(\pi_m\) is the identity homomorphism and \(\pi_0\) is the zero homomorphism). Let \(X_{[m]} = (X_i)_{1 \leq i \leq m}\) be a jointly independent tuple of \(G_m\)-valued random variables. Then

\[ \begin{split} D[ X_{[m]} ] &= \sum_{d=1}^m D[ \pi_d(X_{[m]}) \,|\, \pi_{d-1}(X_{[m]})] \\ &\quad + \sum_{d=1}^{m-1} \mathbb{I}[ \sum_i X_i : \pi_d(X_{[m]}) \; \big| \; \pi_d\big(\sum_i X_i\big), \pi_{d-1}(X_{[m]}) ]. \end{split}\qquad\text{(6)} \]

In particular, by Nonnegativity of conditional mutual information,

\[ \begin{aligned} D[ X_{[m]} ] \geq & \sum_{d=1}^m D[ \pi_d(X_{[m]})|\pi_{d-1}(X_{[m]}) ] \\ & + \mathbb{I}[ \sum_i X_i : \pi_1(X_{[m]}) \; \big| \; \pi_1\bigl(\sum_i X_i\bigr) ].\qquad\text{(7)}\end{aligned} \]

Proof

From Conditional multidistance chain rule (taking \(Y_{[m]} = \pi_{d-1}(X_{[m]})\) and \(\pi = \pi_d\) there, and noting that \(\pi_d(X_{[m]})\) determines \(Y_{[m]}\)) we have

\[ \begin{aligned} D[ X_{[m]} \,|\, \pi_{d-1}(X_{[m]}) ] &= D[ X_{[m]} \,|\, \pi_d(X_{[m]}) ] + D[ \pi_d(X_{[m]})\,|\,\pi_{d-1}(X_{[m]}) ] \\ &\quad + \mathbb{I}[ \sum_{i=1}^m X_i : \pi_d(X_{[m]}) \; \big| \; \pi_d\bigl(\sum_{i=1}^m X_i\bigr), \pi_{d-1}(X_{[m]}) ] \end{aligned} \]

for \(d=1,\dots,m\). The claim follows by telescoping series, noting that \(D[X_{[m]} | \pi_0(X_{[m]})] = D[X_{[m]}]\) and that \(\pi_m(X_{[m]})=X_{[m]}\) (and also \(\pi_m( \sum_i X_i ) = \sum_i X_i\)).

Lean

Formalized as iter_multiDist_chainRule, iter_multiDist_chainRule'.

Sources

Polynomial Freiman-Ruzsa blueprint: chapter/torsion.tex, line 423

Leaniter_multiDist_chainRule · iter_multiDist_chainRule'

Uses 2 · Used by 1

Proof usesConditional multidistance chain rule · Nonnegativity of conditional mutual information

Used bycor-multid

In our application we will need the following special case of the above lemma.

Corollarycor-multid #

Let \(G\) be an abelian group and let \(m \geq 2\). Suppose that \(X_{i,j}\), \(1 \leq i, j \leq m\), are independent \(G\)-valued random variables. Then

\[ \begin{aligned} &\mathbb{I}[ \bigl(\sum_{i=1}^m X_{i,j}\bigr)_{j =1}^{m} : \bigl(\sum_{j=1}^m X_{i,j}\bigr)_{i = 1}^m \; \big| \; \sum_{i=1}^m \sum_{j = 1}^m X_{i,j} ] \\ &\quad \leq \sum_{j=1}^{m-1} \Bigl(D[(X_{i, j})_{i = 1}^m] - D[ (X_{i, j})_{i = 1}^m \; \big| \; (X_{i,j} + \cdots + X_{i,m})_{i =1}^m ]\Bigr) \\ & \qquad\qquad\qquad\qquad + D[(X_{i,m})_{i=1}^m] - D[ \bigl(\sum_{j=1}^m X_{i,j}\bigr)_{i=1}^m ], \end{aligned} \]

where all the multidistances here involve the indexing set \(\{1,\dots, m\}\).

Proof

In Lemma multidist-chain-rule-iter we take \(G_d := G^d\) with the maps \(\pi_d \colon G^m \to G^d\) for \(d=1,\dots,m\) defined by

\[ \pi_d(x_1,\dots,x_m) := (x_1,\dots,x_{d-1}, x_d + \cdots + x_m) \]

with \(\pi_0=0\). Since \(\pi_{d-1}(x)\) can be obtained from \(\pi_{d}(x)\) by applying a homomorphism, we obtain a sequence of the form (5).

Now we apply Lemma multidist-chain-rule-iter with \(I = \{1,\dots, m\}\) and \(X_i := (X_{i,j})_{j = 1}^m\). Using joint independence and Additivity of entropy, we find that

\[ D[ X_{[m]} ] = \sum_{j=1}^m D[ (X_{i,j})_{1 \leq i \leq m} ]. \]

On the other hand, for \(1 \leq j \leq m-1\), we see that once \(\pi_{j}(X_i)\) is fixed, \(\pi_{j+1}(X_i)\) is determined by \(X_{i, j}\) and vice versa, so

\[ D[ \pi_{j+1}(X_{[m]}) \; | \; \pi_{j}(X_{[m]}) ] = D[ (X_{i, j})_{1 \leq i \leq m} \; | \; \pi_{j}(X_{[m]} )]. \]

Since the \(X_{i,j}\) are jointly independent, we may further simplify:

\[ D[ (X_{i, j})_{1 \leq i \leq m} \; | \; \pi_{j}(X_{[m]})] = D[ (X_{i,j})_{1 \leq i \leq m} \; | \; ( X_{i, j} + \cdots + X_{i, m})_{1 \leq i \leq m} ]. \]

Putting all this into the conclusion of Lemma multidist-chain-rule-iter, we obtain

\[ \sum_{j=1}^{m} D[ (X_{i,j})_{1 \leq i \leq m} ] \geq \begin{aligned}[t] &\sum_{j=1}^{m-1} D[ (X_{i,j})_{1 \leq i \leq m} \; | \; (X_{i,j} + \cdots + X_{i,m})_{1 \leq i \leq m} ] \\ &\!\!\!+ D[ \bigl(\sum_{j=1}^m X_{i,j}\bigr)_{1 \leq i \leq m}] \\ &\!\!\!+\mathbb{I}[ \bigl(\sum_{i=1}^m X_{i,j}\bigr)_{j =1}^{m} : \bigl(\sum_{j=1}^m X_{i,j}\bigr)_{i = 1}^m \; \big| \; \sum_{i=1}^m \sum_{j = 1}^m X_{i,j} ] \end{aligned} \]

and the claim follows by rearranging.