Alternate form of submodularity to Entropy of conditionally…

CorollaryAlternate form of submodularity #

With three random variables \(X,Y,Z\), one has

\[ \mathbb{H}[X,Y,Z] + \mathbb{H}[Z] \leq \mathbb{H}[X,Z] + \mathbb{H}[Y,Z]. \]

Uses 2 · Used by 3

Proof usesSubmodularity · Chain rule

Used byImproved Ruzsa triangle inequality · Flipping a sign · torsion-free-doubling

DefinitionIndependent random variables #

Two random variables \(X: \Omega \to S\) and \(Y: \Omega \to T\) are independent if the law of \((X,Y)\) is the product of the law of \(X\) and the law of \(Y\). Similarly for more than two variables.

Lean

Formalized as ProbabilityTheory.IndepFun.

Sources

Polynomial Freiman-Ruzsa blueprint: chapter/entropy.tex, line 241

LeanProbabilityTheory.IndepFun

Used by 2

Used byExistence of independent copies · Vanishing of mutual information

LemmaVanishing of mutual information #

If \(X,Y\) are random variables, then \(\mathbb{I}[X:Y] = 0\) if and only if \(X,Y\) are independent.

Proof

An application of the equality case of Jensen's inequality and Concavity.

Lean

Formalized as ProbabilityTheory.mutualInfo_eq_zero.

Sources

Polynomial Freiman-Ruzsa blueprint: chapter/entropy.tex, line 248

LeanProbabilityTheory.mutualInfo_eq_zero

Uses 3 · Used by 4

Statement usesMutual information · Independent random variables

Proof usesConcavity

Used byIndependent lower bound on sumset · Additivity of entropy · Vanishing conditional mutual information · Zero Ruzsa distance implies large symmetry group

CorollaryAdditivity of entropy #

If \(X,Y\) are random variables, then \(\mathbb{H}[X,Y] = \mathbb{H}[X] + \mathbb{H}[Y]\) if and only if \(X,Y\) are independent.

Proof

Direct from Vanishing of mutual information.

Lean

Formalized as ProbabilityTheory.entropy_pair_eq_add.

Sources

Polynomial Freiman-Ruzsa blueprint: chapter/entropy.tex, line 263

LeanProbabilityTheory.entropy_pair_eq_add

Uses 1 · Used by 6

Proof usesVanishing of mutual information

Used byImproved Ruzsa triangle inequality · Balog-Szemerédi-Gowers · Kaimanovich-Vershik-Madiman inequality · Specific fibring identity · Flipping a sign · cor-multid

DefinitionConditional mutual information #

If \(X,Y,Z\) are random variables, with \(Z\) \(U\)-valued, then

\[ \mathbb{I}[X:Y|Z] := \sum_{z \in U} P[Z=z] \mathbb{I}[(X|Z=z): (Y|Z=z)]. \]

Lean

Formalized as ProbabilityTheory.condMutualInfo.

Sources

Polynomial Freiman-Ruzsa blueprint: chapter/entropy.tex, line 273

LeanProbabilityTheory.condMutualInfo

Uses 2 · Used by 5

Statement usesMutual information · Conditioned event

Used byConditional lower bound on sumset · Bound on conditional mutual informations · Alternate formula for conditional mutual information · Nonnegativity of conditional mutual information · Data processing inequality

LemmaAlternate formula for conditional mutual information #

We have

\[ \mathbb{I}[X:Y|Z] := \mathbb{H}[X|Z] + \mathbb{H}[Y|Z] - \mathbb{H}[X,Y|Z] \]

and

\[ \mathbb{I}[X:Y|Z] := \mathbb{H}[X|Z] - \mathbb{H}[X|Y,Z]. \]

Proof

Routine computation.

Lean

Formalized as ProbabilityTheory.condMutualInfo_eq, ProbabilityTheory.condMutualInfo_eq'.

Sources

Polynomial Freiman-Ruzsa blueprint: chapter/entropy.tex, line 282

LeanProbabilityTheory.condMutualInfo_eq · ProbabilityTheory.condMutualInfo_eq'

Uses 1 · Used by 4

Statement usesConditional mutual information

Used bySymmetry identity · Entropy of conditionally independent variables · General fibring identity · Multidistance chain rule

LemmaNonnegativity of conditional mutual information #

If \(X,Y,Z\) are random variables, then \(\mathbb{I}[X:Y|Z] \ge 0\).

Proof

Use Conditional mutual information and Submodularity.

Lean

Formalized as ProbabilityTheory.condMutualInfo_nonneg.

Sources

Polynomial Freiman-Ruzsa blueprint: chapter/entropy.tex, line 295

LeanProbabilityTheory.condMutualInfo_nonneg

Uses 2 · Used by 1

Statement usesConditional mutual information

Proof usesSubmodularity

Used bymultidist-chain-rule-iter

DefinitionConditionally independent random variables #

Two random variables \(X: \Omega \to S\) and \(Y: \Omega \to T\) are conditionally independent relative to another random variable \(Z: \Omega \to U\) if \(P[X = s \wedge Y = t| Z=u] = P[X=s|Z=u] P[Y=t|Z=u]\) for all \(s \in S, t \in T, u \in U\). (We won't need conditional independence for more variables than this.)