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
Moreover, if \(Z_1,Z_2\) are taken to be independent, then the difference between the two sides is
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
In the middle step, we used Submodularity, and in the last step we used the fact that
(thanks to Chain rule and Entropy and relabeling) and that
(since \(Z_i\) determines \(\pi(Z_i)\)). This gives the claimed inequality. The difference between the two sides is precisely
To rewrite this in terms of (conditional) mutual information, we use the identity
(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
Proof
By General fibring identity and the nonnegativity of conditional Ruzsa distance (from Distance nonnegative) we have
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
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)
while by definition
Furthermore,
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
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
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.