Data processing inequality

LemmaData processing for a single variable#

Let \(X\) be a random variable. Then for any function \(f\) on the range of \(X\), one has \(\mathbb{H}[f(X)] \leq \mathbb{H}[X]\).

Proof

We have

\[ \mathbb{H}[X] = \mathbb{H}[X,f(X)] = \mathbb{H}[f(X)] + \mathbb{H}[X|f(X)] \]

thanks to Entropy and relabeling and Chain rule, giving the claim.

Lean

Formalized as ProbabilityTheory.entropy_comp_le.

Sources

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

LeanProbabilityTheory.entropy_comp_le

Uses 2 · Used by 1

Proof usesEntropy and relabeling · Chain rule

Used byFlipping a sign

LemmaOne-sided unconditional data processing inequality#

Let \(X,Y\) be random variables. For any function \(f, g\) on the range of \(X\), we have \(\mathbb{I}[f(X) : Y] \leq \mathbb{I}[X:Y]\).

Proof

By Alternative formulae for mutual information it suffices to show that \(\mathbb{H}[Y|X] \leq \mathbb{H}[Y|f(X)]\). But this follows from Submodularity (and Entropy and relabeling).

Lean

Formalized as ProbabilityTheory.mutual_comp_le.

Sources

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

LeanProbabilityTheory.mutual_comp_le

Uses 3 · Used by 1

Proof usesAlternative formulae for mutual information · Submodularity · Entropy and relabeling

Used byUnconditional data processing inequality

LemmaUnconditional data processing inequality#

Let \(X,Y\) be random variables. For any functions \(f, g\) on the ranges of \(X, Y\) respectively, we have \(\mathbb{I}[f(X) : g(Y )] \leq \mathbb{I}[X : Y]\).

Proof

From One-sided unconditional data processing inequality, Commutativity and associativity of joint entropy we have \(\mathbb{I}[f(X) : Y] \leq \mathbb{I}[X:Y]\) and \(\mathbb{I}[f(X): g(Y)] \leq \mathbb{I}[f(X):Y]\), giving the claim.

Lean

Formalized as ProbabilityTheory.mutual_comp_comp_le.

Sources

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

LeanProbabilityTheory.mutual_comp_comp_le

Uses 2 · Used by 1

Proof usesOne-sided unconditional data processing inequality · Commutativity and associativity of joint entropy

Used byData processing inequality

LemmaData processing inequality#

Let \(X,Y,Z\). For any functions \(f, g\) on the ranges of \(X, Y\) respectively, we have \(\mathbb{I}[f(X) : g(Y )|Z] \leq \mathbb{I}[X :Y |Z]\).

Proof

Apply Unconditional data processing inequality to \(X,Y\) conditioned to the event \(Z=z\), multiply by \({\bf P}[Z=z]\), and sum using Conditional mutual information.

Lean

Formalized as ProbabilityTheory.condMutual_comp_comp_le.

Sources

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

LeanProbabilityTheory.condMutual_comp_comp_le

Uses 2 · Used by 1

Proof usesUnconditional data processing inequality · Conditional mutual information

Used byMutual information bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.