The Fibring lemma

PropositionGeneral fibring identity#

Let \(\pi : H \to H'\) be a homomorphism additive groups, and let \(Z_1,Z_2\) be \(H\)-valued random variables. Then we have

\[ d[Z_1; Z_2] \geq d[\pi(Z_1);\pi(Z_2)] + d[Z_1|\pi(Z_1); Z_2 |\pi(Z_2)]. \]

Moreover, if \(Z_1,Z_2\) are taken to be independent, then the difference between the two sides is

\[ I( Z_1 - Z_2 : (\pi(Z_1), \pi(Z_2)) | \pi(Z_1 - Z_2) ). \]
Proof

Let \(Z_1,Z_2\) be independent throughout (this is possible by Copy preserves Ruzsa distance and Existence of independent copies). By Alternate form of distance, We have

\[ \begin{aligned} & d[Z_1 |\pi(Z_1); Z_2 |\pi(Z_2)] \\ & = \mathbb{H}[Z_1 - Z_2 | \pi(Z_1),\pi(Z_2)] - \tfrac{1}{2} \mathbb{H}[Z_1 | \pi(Z_1)] - \tfrac{1}{2} \mathbb{H}[Z_2 | \pi(Z_2)] \\ & \leq \mathbb{H}[Z_1 - Z_2 | \pi(Z_1+Z_2)] - \tfrac{1}{2} \mathbb{H}[Z_1 | \pi(Z_1)] - \tfrac{1}{2}H[Z_2 | \pi(Z_2)] \\ & = d[Z_1;Z_2] - d[\pi(Z_1);\pi(Z_2)]. \end{aligned} \]

In the middle step, we used Submodularity, and in the last step we used the fact that

\[ \mathbb{H}[Z_1 - Z_2 | \pi(Z_1-Z_2)] = \mathbb{H}[Z_1 - Z_2] - \mathbb{H}[\pi(Z_1-Z_2)] \]

(thanks to Chain rule and Entropy and relabeling) and that

\[ \mathbb{H}[Z_i| \pi(Z_i)] = \mathbb{H}[Z_i] - \mathbb{H}[\pi(Z_i)] \]

(since \(Z_i\) determines \(\pi(Z_i)\)). This gives the claimed inequality. The difference between the two sides is precisely

\[ \mathbb{H}[Z_1 - Z_2 | \pi(Z_1 - Z_2)] - \mathbb{H}[Z_1 - Z_2 | \pi(Z_1),\pi(Z_2)]. \]

To rewrite this in terms of (conditional) mutual information, we use the identity

\[ \mathbb{H}[A|B] - \mathbb{H}[A | B,C] = \mathbb{I}[A : C | B], \]

(which follows Alternate formula for conditional mutual information) taking \(A := Z_1 - Z_2\), \(B := \pi(Z_1 - Z_2)\) and \(C := (\pi(Z_1),\pi(Z_{2}))\), and noting that in this case \(\mathbb{H}[A | B,C] = \mathbb{H}[A | C]\) since \(C\) uniquely determines \(B\) (this may require another helper lemma about entropy). This completes the proof.

Lean

Formalized as rdist_of_indep_eq_sum_fibre, rdist_le_sum_fibre.

Sources
Uses 7 · Used by 3

Corollaryfibring-ineq#

If \(\pi:G\to H\) is a homomorphism of additive groups and \(X,Y\) are \(G\)-valued random variables then

\[ d[X;Y]\geq d[\pi(X);\pi(Y)]. \]
Proof

By General fibring identity and the nonnegativity of conditional Ruzsa distance (from Distance nonnegative) we have

\[ d[X;Y]\geq d[\pi(X);\pi(Y)]+d[X\mid \pi(X);Y\mid \pi(Y)]. \]

The inequality follows from \(d[X\mid \pi(X);Y\mid \pi(Y)]\geq 0\) (Distance nonnegative).

Lean

Formalized as rdist_of_hom_le.

Sources
Uses 2 · Used by 1

CorollarySpecific fibring identity#

Let \(Y_1,Y_2,Y_3\) and \(Y_4\) be independent \(G\)-valued random variables. Then

\[ \begin{aligned} & d[Y_1+Y_3; Y_2+Y_4] + d[Y_1|Y_1+Y_3; Y_2|Y_2+Y_4] \\ &\qquad + \mathbb{I}[Y_1+Y_2 : Y_2 + Y_4 | Y_1+Y_2+Y_3+Y_4] = d[Y_1; Y_2] + d[Y_3; Y_4]. \end{aligned} \]
Proof

We apply General fibring identity with \(H := G \times G\), \(H' := G\), \(\pi\) the addition homomorphism \(\pi(x,y) := x+y\), and with the random variables \(Z_1 := (Y_1,Y_3)\) and \(Z_2 := (Y_2,Y_4)\). Then by independence (Additivity of entropy)

\[ d[Z_1; Z_2] = d[Y_1; Y_2] + d[Y_3; Y_4] \]

while by definition

\[ d[\pi(Z_1); \pi(Z_2)] = d[Y_1+Y_3; Y_2+Y_4]. \]

Furthermore,

\[ d[Z_1|\pi(Z_1); Z_2|\pi(Z_2)] = d[Y_1|Y_1+Y_3;Y_2|Y_2+Y_4], \]

since \(Z_1=(Y_1,Y_3)\) and \(Y_1\) are linked by an invertible affine transformation once \(\pi(Z_1)=Y_1+Y_3\) is fixed, and similarly for \(Z_2\) and \(Y_2\). (This has to do with Conditional entropy and relabeling) Finally, we have

\[ \begin{aligned} &\mathbb{I}[Z_1 + Z_2 : (\pi(Z_1),\pi(Z_2)) \,|\, \pi(Z_1) + \pi(Z_2)] \\ &\ = \mathbb{I}[(Y_1+Y_2, Y_3+Y_4) : (Y_1+Y_3, Y_2+Y_4) \,|\, Y_1+Y_2+Y_3+Y_4] \\ &\ = \mathbb{I}[Y_1+Y_2 : Y_2+Y_4 \,|\, Y_1+Y_2+Y_3+Y_4] \end{aligned} \]

where in the last line we used the fact that \((Y_1+Y_2, Y_1+Y_2+Y_3+Y_4)\) uniquely determine \(Y_3+Y_4\) and similarly \((Y_2+Y_4, Y_1+Y_2+Y_3+Y_4)\) uniquely determine \(Y_1+Y_3\). (This requires another helper lemma about entropy.)

Lean

Formalized as sum_of_rdist_eq.

Sources
Uses 3 · Used by 6

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.