Entropy to Submodularity

DefinitionEntropy #

If \(X\) is an \(S\)-valued random variable, the entropy \(\mathbb{H}[X]\) of \(X\) is defined

\[ \mathbb{H}[X] := \sum_{s \in S} \mathbb{P}[X=x] \log \frac{1}{\mathbb{P}[X=x]} \]

with the convention that \(0 \log \frac{1}{0} = 0\).

Lean

Formalized as ProbabilityTheory.entropy.

Sources

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

LeanProbabilityTheory.entropy

Used by 9

Used byCopy preserves entropy · Ruzsa distance · Bounded entropy implies concentration · Conditional entropy · Mutual information · Jensen bound · Entropy and relabeling · Entropy of uniform random variable · Entropy of uniform random variable, II

LemmaEntropy and relabeling #

(i) If \(X: \Omega \to S\) and \(Y: \Omega \to T\) are random variables, and \(Y = f(X)\) for some injection \(f: S \to T\), then \(\mathbb{H}[X] = \mathbb{H}[Y]\).
(ii) If \(X: \Omega \to S\) and \(Y: \Omega \to T\) are random variables, and \(Y = f(X)\) and \(X = g(Y)\) for some functions \(f: S \to T\), \(g: T \to S\), then \(\mathbb{H}[X] = \mathbb{H}[Y]\).

Proof

Expand out both entropies and rearrange.

Lean

Formalized as ProbabilityTheory.entropy_comp_of_injective, ProbabilityTheory.entropy_of_comp_eq_of_comp.

Sources

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

LeanProbabilityTheory.entropy_comp_of_injective · ProbabilityTheory.entropy_of_comp_eq_of_comp

Uses 1 · Used by 14

Statement usesEntropy

Used byNegation preserves entropy · Ruzsa distance in independent case · Improved Ruzsa triangle inequality · Balog-Szemerédi-Gowers · Comparison of Ruzsa distances, I · Kaimanovich-Vershik-Madiman inequality · Commutativity and associativity of joint entropy · Conditional entropy and relabeling · General fibring identity · Data processing for a single variable · One-sided unconditional data processing inequality · Application of BSG · Flipping a sign · Multidistance chain rule

LemmaJensen bound #

If \(X\) is an \(S\)-valued random variable, then \(\mathbb{H}[X] \leq \log |S|\).

Proof

This is a direct consequence of Concavity and Jensen's inequality.

Lean

Formalized as ProbabilityTheory.entropy_le_log_card, ProbabilityTheory.entropy_le_log_card_of_mem.

Sources

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

LeanProbabilityTheory.entropy_le_log_card · ProbabilityTheory.entropy_le_log_card_of_mem

Uses 2 · Used by 4

Statement usesEntropy

Proof usesConcavity

Used byProjection entropy and distance · pfr_aux-improv · pfr_aux · pfr_aux_torsion

DefinitionUniform distribution #

If \(H\) is a subset of \(S\), an \(S\)-random variable \(X\) is said to be uniformly distributed on \(H\) if \(\mathbb{P}[X = s] = 1/|H|\) for \(s \in X\) and \(\mathbb{P}[X=s] = 0\) otherwise.

Lean

Formalized as ProbabilityTheory.IsUniform.

Sources

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

LeanProbabilityTheory.IsUniform

Used by 3

Used byUniform distributions exist · Entropy of uniform random variable, II · Translate is uniform on symmetry group

LemmaUniform distributions exist #

Given a finite non-empty subset \(H\) of a set \(S\), there exists a random variable \(X\) (on some probability space) that is uniformly distributed on \(H\).

Proof

Direct construction.

Lean

Formalized as ProbabilityTheory.exists_isUniform, ProbabilityTheory.exists_isUniform_measureSpace.

Sources

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

LeanProbabilityTheory.exists_isUniform · ProbabilityTheory.exists_isUniform_measureSpace

Uses 1 · Used by 3

Statement usesUniform distribution

Used bypfr_aux-improv · pfr_aux · pfr_aux_torsion

LemmaEntropy of uniform random variable #

If \(X\) is \(S\)-valued random variable, then \(\mathbb{H}[X] = \log |S|\) if and only if \(X\) is uniformly distributed on \(S\).

Proof

Direct computation in one direction. Converse direction needs the strict Jensen inequality and Concavity.

Lean

Formalized as ProbabilityTheory.IsUniform.entropy_eq.

Sources

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

LeanProbabilityTheory.IsUniform.entropy_eq

Uses 2

Statement usesEntropy

Proof usesConcavity

LemmaEntropy of uniform random variable, II #

If \(X\) is uniformly distributed on \(H\), then, then \(\mathbb{H}[X] = \log |H|\).

Proof

Direct computation.

Lean

Formalized as ProbabilityTheory.IsUniform.entropy_eq.

Sources

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

LeanProbabilityTheory.IsUniform.entropy_eq

Uses 2 · Used by 3

Statement usesEntropy · Uniform distribution

Used bypfr_aux-improv · pfr_aux · pfr_aux_torsion

LemmaBounded entropy implies concentration #

If \(X\) is an \(S\)-valued random variable, then there exists \(s \in S\) such that \(\mathbb{P}[X=s] \geq \exp(-\mathbb{H}[X])\).

Proof

We have

\[ \mathbb{H}[X] = \sum_{s \in S} \mathbb{P}[X=s] \log \frac{1}{\mathbb{P}[X=s]} \geq \min_{s \in S} \log \frac{1}{\mathbb{P}[X=s]} \]

and the claim follows.

Lean

Formalized as ProbabilityTheory.prob_ge_exp_neg_entropy.

Sources

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

LeanProbabilityTheory.prob_ge_exp_neg_entropy

Uses 1 · Used by 3

Statement usesEntropy

Used bypfr_aux-improv · pfr_aux · pfr_aux_torsion

We use \(X,Y\) to denote the pair \(\omega \mapsto (X(\omega),Y(\omega)\)).

LemmaCommutativity and associativity of joint entropy #

If \(X: \Omega \to S\), \(Y: \Omega \to T\), and \(Z: \Omega \to U\) are random variables, then \(\mathbb{H}[X, Y] = \mathbb{H}[Y, X]\) and \(\mathbb{H}[X, (Y,Z)] = \mathbb{H}[(X,Y), Z]\).

Proof

Set up an injection from \((X,Y)\) to \((Y,X)\) and use Entropy and relabeling for the first claim. Similarly for the second claim.

Lean

Formalized as ProbabilityTheory.entropy_comm, ProbabilityTheory.entropy_assoc.

Sources

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

LeanProbabilityTheory.entropy_comm · ProbabilityTheory.entropy_assoc

Uses 1 · Used by 2

Proof usesEntropy and relabeling

Used byAlternative formulae for mutual information · Unconditional data processing inequality

DefinitionConditioned event #

If \(X: \Omega \to S\) is an \(S\)-valued random variable and \(E\) is an event in \(\Omega\), then the conditioned event \((X|E)\) is defined to be the same random variable as \(X\), but now the ambient probability measure has been conditioned to \(E\).

Lean

Formalized as ProbabilityTheory.cond.

Sources

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

LeanProbabilityTheory.cond

Used by 2

Used byConditional entropy · Conditional mutual information

Note: it may happen that \(E\) has zero measure. In which case, the ambient probability measure should be replaced with a zero measure. (In our formalization we achieve this by working with arbitrary measures, and normalizing them to be probability measures if possible, else using the zero measure. Conditioning is also formalized using existing Mathlib definitions.)

DefinitionConditional entropy #

If \(X: \Omega \to S\) and \(Y: \Omega \to T\) are random variables, the conditional entropy \(\mathbb{H}[X|Y]\) is defined as

\[ \mathbb{H}[X|Y] := \sum_{y \in Y} \mathbb{P}[Y = y] \mathbb{H}[(X | Y=y)]. \]

Lean

Formalized as ProbabilityTheory.condEntropy.

Sources

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

LeanProbabilityTheory.condEntropy

Uses 2 · Used by 5

Statement usesEntropy · Conditioned event

Used byAlternate form of distance · Balog-Szemerédi-Gowers · Chain rule · Conditional entropy and relabeling · Alternate form of conditional multidistance

LemmaConditional entropy and relabeling #

If \(X: \Omega \to S\), \(Y: \Omega \to T\), and \(Z: \Omega \to U\) are random variables, and \(Y = f(X,Z)\) almost surely for some map \(f: S \times U \to T\) that is injective for each fixed \(U\), then \(\mathbb{H}[X|Z] = \mathbb{H}[Y|Z]\).

Similarly, if \(g: T \to U\) is injective, then \(\mathbb{H}[X|g(Y)] = \mathbb{H}[X|Y]\).

Proof

For the first part, use Conditional entropy and then Entropy and relabeling. The second part is a direct computation.

Lean

Formalized as ProbabilityTheory.condEntropy_comp_of_injective, ProbabilityTheory.condEntropy_of_injective'.

Sources

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

LeanProbabilityTheory.condEntropy_comp_of_injective · ProbabilityTheory.condEntropy_of_injective'

Uses 2 · Used by 4

Statement usesConditional entropy

Proof usesEntropy and relabeling

Used byShearing preserves entropy · Bound on distance differences · Zero Ruzsa distance implies large symmetry group · Specific fibring identity

LemmaChain rule #

If \(X: \Omega \to S\) and \(Y: \Omega \to T\) are random variables, then

\[ \mathbb{H}[X, Y] = \mathbb{H}[Y] + \mathbb{H}[X|Y]. \]

Proof

Direct computation.

Lean

Formalized as ProbabilityTheory.chain_rule, ProbabilityTheory.chain_rule'.

Sources

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

LeanProbabilityTheory.chain_rule · ProbabilityTheory.chain_rule'

Uses 1 · Used by 9

Statement usesConditional entropy

Used byProjection entropy and distance · Shearing preserves entropy · Symmetry identity · Alternative formulae for mutual information · Conditional chain rule · Alternate form of submodularity · General fibring identity · Data processing for a single variable · Multidistance chain rule

LemmaConditional chain rule #

If \(X: \Omega \to S\), \(Y: \Omega \to T\), \(Z: \Omega \to U\) are random variables, then

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

Proof

For each \(z \in U\), we can apply Chain rule to the random variables \((X|Z=z)\) and \((Y|Z=z)\) to obtain

\[ \mathbb{H}[(X|Z=z),(Y|Z=z)] = \mathbb{H}[Y|Z=z] + \mathbb{H}[(X|Z=z)|(Y|Z=z)]. \]

Now multiply by \(\mathbb{P}[Z=z]\) and sum. Some helper lemmas may be needed to get to the form above. This sort of “average over conditioning” argument to get conditional entropy inequalities from unconditional ones is commonly used in this paper.