Negation preserves entropy to Alternate form of distance

LemmaNegation preserves entropy#

If \(X\) is \(G\)-valued, then \(\mathbb{H}[-X]=\mathbb{H}[X]\).

Proof

Immediate from Entropy and relabeling.

Lean

Formalized as ProbabilityTheory.entropy_neg.

Sources
LeanProbabilityTheory.entropy_neg
Uses 1 · Used by 9
Proof usesEntropy and relabeling
Used byDistance controls entropy difference · Distance controls entropy growth · Distance symmetric · Lower bound of sumset · Comparing sums · Kaimonovich–Vershik–Madiman inequality, II · Flipping a sign · Sums of dilates I · Multidistance and Ruzsa distance, III

LemmaShearing preserves entropy#

If \(X,Y\) are \(G\)-valued, then \(\mathbb{H}[X \pm Y | Y]=\mathbb{H}[X|Y]\) and \(\mathbb{H}[X \pm Y, Y] = \mathbb{H}[X, Y]\).

Proof

Immediate from Conditional entropy and relabeling and Chain rule.

Lean

Formalized as ProbabilityTheory.condEntropy_add_right, ProbabilityTheory.condEntropy_add_left, ProbabilityTheory.condEntropy_sub_right, ProbabilityTheory.condEntropy_sub_left.

Sources
LeanProbabilityTheory.condEntropy_add_right · ProbabilityTheory.condEntropy_add_left · ProbabilityTheory.condEntropy_sub_right · ProbabilityTheory.condEntropy_sub_left
Uses 2 · Used by 2
Proof usesConditional entropy and relabeling · Chain rule
Used byProjection entropy and distance · Lower bound of sumset

LemmaLower bound of sumset#

If \(X,Y\) are \(G\)-valued random variables on \(\Omega\), we have

\[ \max(\mathbb{H}[X], \mathbb{H}[Y]) - \mathbb{I}[X:Y] \leq \mathbb{H}[X \pm Y]. \]
Proof

By Conditioning reduces entropy, Shearing preserves entropy, Alternative formulae for mutual information, Negation preserves entropy we have

\[ \mathbb{H}[X\pm Y] \geq \mathbb{H}[X\pm Y|Y] = \mathbb{H}[X|Y]= \mathbb{H}[X] - \mathbb{I}[X:Y] \]

and similarly with the roles of \(X,Y\) reversed, giving the claim.

Lean

Formalized as ProbabilityTheory.max_entropy_sub_mutualInfo_le_entropy_add, ProbabilityTheory.max_entropy_sub_mutualInfo_le_entropy_sub.

Sources
LeanProbabilityTheory.max_entropy_sub_mutualInfo_le_entropy_add · ProbabilityTheory.max_entropy_sub_mutualInfo_le_entropy_sub
Uses 4 · Used by 2
Proof usesConditioning reduces entropy · Alternative formulae for mutual information · Shearing preserves entropy · Negation preserves entropy
Used byIndependent lower bound on sumset · Conditional lower bound on sumset

CorollaryConditional lower bound on sumset#

If \(X,Y\) are \(G\)-valued random variables on \(\Omega\) and \(Z\) is another random variable on \(\Omega\) then

\[ \max(\mathbb{H}[X|Z], \mathbb{H}[Y|Z]) - \mathbb{I}[X:Y|Z] \leq \mathbb{H}[X\pm Y|Z], \]
Proof

This follows from Lower bound of sumset by conditioning to \(Z = z\) and summing over \(z\) (weighted by \(\mathbb{P}[Z=z]\)).

Lean

Formalized as ProbabilityTheory.max_condEntropy_sub_condMutualInfo_le_condEntropy_mul, ProbabilityTheory.max_condEntropy_sub_condMutualInfo_le_condEntropy_div.

Sources
LeanProbabilityTheory.max_condEntropy_sub_condMutualInfo_le_condEntropy_mul · ProbabilityTheory.max_condEntropy_sub_condMutualInfo_le_condEntropy_div
Uses 2
Statement usesConditional mutual information
Proof usesLower bound of sumset

CorollaryIndependent lower bound on sumset#

If \(X,Y\) are independent \(G\)-valued random variables, then

\[ \max(\mathbb{H}[X], \mathbb{H}[Y]) \leq \mathbb{H}[X\pm Y]. \]
Proof

Combine Lower bound of sumset with Vanishing of mutual information.

Lean

Formalized as ProbabilityTheory.max_entropy_le_entropy_add, ProbabilityTheory.max_entropy_le_entropy_sub.

Sources
LeanProbabilityTheory.max_entropy_le_entropy_add · ProbabilityTheory.max_entropy_le_entropy_sub
Uses 2 · Used by 9
Proof usesLower bound of sumset · Vanishing of mutual information
Used byDistance controls entropy difference · Distance controls entropy growth · Bounding mutual information · Comparing sums · Kaimonovich–Vershik–Madiman inequality, II · Nonnegativity · Multidistance and Ruzsa distance, I · Multidistance and Ruzsa distance, III · Multidistance and Ruzsa distance, IV

One random variable is said to be a copy of another if they have the same distribution.

LemmaCopy preserves entropy#

If \(X'\) is a copy of \(X\) then \(\mathbb{H}[X'] = \mathbb{H}[X]\).

Proof

Immediate from Entropy.

Lean

Formalized as ProbabilityTheory.IdentDistrib.entropy_congr.

Sources
LeanProbabilityTheory.IdentDistrib.entropy_congr
Uses 1 · Used by 6
Statement usesEntropy
Used byAlternate form of distance · Copy preserves Ruzsa distance · Ruzsa distance in independent case · Balog-Szemerédi-Gowers · Symmetry identity · \(\tau\) depends only on distribution

LemmaExistence of independent copies#

Let \(X_i : \Omega_i \to S_i\) be random variables for \(i=1,\dots,k\). Then if one gives \(\prod_{i=1}^k S_i\) the product measure of the laws of \(X_i\), the coordinate functions \((x_j)_{j=1}^k \mapsto x_i\) are jointly independent random variables which are copies of the \(X_1,\dots,X_k\).

Proof

Explicit computation.

Lean

Formalized as ProbabilityTheory.independent_copies, ProbabilityTheory.independent_copies', ProbabilityTheory.independent_copies_two, ProbabilityTheory.independent_copies3_nondep.

Sources
LeanProbabilityTheory.independent_copies · ProbabilityTheory.independent_copies' · ProbabilityTheory.independent_copies_two · ProbabilityTheory.independent_copies3_nondep
Uses 1 · Used by 9
Statement usesIndependent random variables
Used byProjection entropy and distance · Ruzsa distance · Ruzsa triangle inequality · Upper bound on conditioned Ruzsa distance · Comparison of Ruzsa distances, I · Zero Ruzsa distance implies large symmetry group · General fibring identity · Flipping a sign · Multidistance and Ruzsa distance, IV

DefinitionRuzsa distance#

Let \(X,Y\) be \(G\)-valued random variables (not necessarily on the same sample space). The Ruzsa distance \(d[X ;Y]\) between \(X\) and \(Y\) is defined to be

\[ d[X ;Y] := \mathbb{H}[X' - Y'] - \mathbb{H}[X']/2 - \mathbb{H}[Y']/2 \]

where \(X',Y'\) are (the canonical) independent copies of \(X,Y\) from Existence of independent copies.

Lean

Formalized as rdist_def.

Sources
Leanrdist_def
Uses 2 · Used by 11
Statement usesEntropy · Existence of independent copies
Used byConditioned Ruzsa distance · Distance from zero · Copy preserves Ruzsa distance · Ruzsa distance in independent case · Distance controls entropy difference · Distance controls entropy growth · Distance symmetric · \(\tau\) functional · pfr_aux-improv · pfr_aux · pfr_aux_torsion

LemmaDistance from zero#

If \(X\) is a \(G\)-valued random variable and \(0\) is the random variable taking the value \(0\) everywhere then

\[ d[X;0]=\mathbb{H}(X)/2. \]
Proof

This is an immediate consequence of the definitions and \(X-0\equiv X\) and \(\mathbb{H}(0)=0\).

Lean

Formalized as rdist_zero_eq_half_ent.

Sources
Leanrdist_zero_eq_half_ent
Uses 1 · Used by 1
Statement usesRuzsa distance
Used bytorsion-dist-shrinking

LemmaCopy preserves Ruzsa distance#

If \(X',Y'\) are copies of \(X,Y\) respectively then \(d[X';Y']=d[X ;Y]\).

Proof

Immediate from Definitions Ruzsa distance and Copy preserves entropy.

Lean

Formalized as ProbabilityTheory.IdentDistrib.rdist_congr.

Sources
LeanProbabilityTheory.IdentDistrib.rdist_congr
Uses 2 · Used by 8
Statement usesRuzsa distance
Proof usesCopy preserves entropy
Used byAlternate form of distance · Ruzsa triangle inequality · Comparison of Ruzsa distances, I · Zero Ruzsa distance implies large symmetry group · General fibring identity · Flipping a sign · Multidistance and Ruzsa distance, I · Multidistance and Ruzsa distance, III

LemmaRuzsa distance in independent case#

If \(X,Y\) are independent \(G\)-random variables then

\[ d[X ;Y] := \mathbb{H}[X - Y] - \mathbb{H}[X]/2 - \mathbb{H}[Y]/2. \]
Proof

Immediate from Ruzsa distance and Lemmas Entropy and relabeling, Copy preserves entropy.

Lean

Formalized as ProbabilityTheory.IndepFun.rdist_eq.

Sources
LeanProbabilityTheory.IndepFun.rdist_eq
Uses 3 · Used by 14
Statement usesRuzsa distance
Proof usesEntropy and relabeling · Copy preserves entropy
Used byAlternate form of distance · Ruzsa triangle inequality · Balog-Szemerédi-Gowers · Comparison of Ruzsa distances, I · Entropy bound on quadruple sum · second-estimate-aux · Zero Ruzsa distance implies large symmetry group · Kaimonovich–Vershik–Madiman inequality, II · Kaimonovich–Vershik–Madiman inequality, III · Flipping a sign · Sums of dilates II · Multidistance and Ruzsa distance, I · Multidistance and Ruzsa distance, III · Multidistance and Ruzsa distance, IV

LemmaDistance symmetric#

If \(X,Y\) are \(G\)-valued random variables, then

\[ d[X ;Y] = d[Y;X]. \]
Proof

Immediate from Negation preserves entropy and Ruzsa distance.

Lean

Formalized as rdist_symm.

Sources
Leanrdist_symm
Uses 2
Statement usesRuzsa distance
Proof usesNegation preserves entropy

LemmaDistance controls entropy difference#

If \(X,Y\) are \(G\)-valued random variables, then

\[ |\mathbb{H}[X]-H[Y]| \leq 2 d[X ;Y]. \]
Proof

Immediate from Independent lower bound on sumset and Ruzsa distance, and also Negation preserves entropy.

Lean

Formalized as diff_ent_le_rdist.

Sources
Leandiff_ent_le_rdist
Uses 3 · Used by 8
Statement usesRuzsa distance
Proof usesIndependent lower bound on sumset · Negation preserves entropy
Used byProjection entropy and distance · Distance nonnegative · pfr_aux-improv · pfr_aux · Kaimonovich–Vershik–Madiman inequality, II · pfr_aux_torsion · app-ent-pfr · torsion-free-doubling

LemmaDistance controls entropy growth#

If \(X,Y\) are independent \(G\)-valued random variables, then

\[ \mathbb{H}[X-Y] - \mathbb{H}[X], \mathbb{H}[X-Y] - \mathbb{H}[Y] \leq 2d[X ;Y]. \]
Proof

Immediate from Independent lower bound on sumset and Ruzsa distance, and also Negation preserves entropy.

Lean

Formalized as diff_ent_le_rdist'.

Sources
Leandiff_ent_le_rdist' · diff_ent_le_rdist''
Uses 3
Statement usesRuzsa distance
Proof usesIndependent lower bound on sumset · Negation preserves entropy

LemmaDistance nonnegative#

If \(X,Y\) are \(G\)-valued random variables, then

\[ d[X ;Y] \geq 0. \]
Proof

Immediate from Distance controls entropy difference.

Lean

Formalized as rdist_nonneg.

Sources
Leanrdist_nonneg
Uses 1 · Used by 4
Proof usesDistance controls entropy difference
Used byGeneral 100% inverse theorem · fibring-ineq · Vanishing · app-ent-pfr

LemmaProjection entropy and distance#

If \(G\) is an additive group and \(X\) is a \(G\)-valued random variable and \(H\leq G\) is a finite subgroup then, with \(\pi:G\to G/H\) the natural homomorphism we have (where \(U_H\) is uniform on \(H\))

\[ \mathbb{H}(\pi(X))\leq 2d[X;U_H]. \]
Proof

WLOG, we make \(X\), \(U_H\) independent (Existence of independent copies). Now by Lemmas Submodularity, Shearing preserves entropy, Jensen bound

\[ \begin{aligned} &\mathbb{H}(X-U_H|\pi(X)) \geq \mathbb{H}(X-U_H|X) &= \mathbb{H}(U_H) \\ &\mathbb{H}(X-U_H|\pi(X)) \leq \log |H| &= \mathbb{H}(U_H) \end{aligned} \]

By Chain rule

\[ \mathbb{H}(X-U_H)=\mathbb{H}(\pi(X))+\mathbb{H}(X-U_H|\pi(X))=\mathbb{H}(\pi(X))+\mathbb{H}(U_H) \]

and therefore

\[ d[X;U_H]=\mathbb{H}(\pi(X))+\frac{\mathbb{H}(U_H)-\mathbb{H}(X)}{2}. \]

Furthermore by Distance controls entropy difference

\[ d[X;U_H]\geq \frac{\lvert \mathbb{H}(X)-\mathbb{H}(U_H)\rvert}{2}. \]

Adding these inequalities gives the result.

Lean

Formalized as ent_of_proj_le.

Sources
Leanent_of_proj_le
Uses 6 · Used by 1
Proof usesExistence of independent copies · Distance controls entropy difference · Chain rule · Shearing preserves entropy · Submodularity · Jensen bound
Used byapp-ent-pfr

LemmaImproved Ruzsa triangle inequality#

If \(X,Y,Z\) are \(G\)-valued random variables on \(\Omega\) with \((X,Y)\) independent of \(Z\), then

\[ \mathbb{H}[X - Y] \leq \mathbb{H}[X-Z] + \mathbb{H}[Z-Y] - \mathbb{H}[Z]\qquad\text{(1)} \]
Proof

Apply Alternate form of submodularity to obtain

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

Using

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

(from Entropy and relabeling, Subadditivity),

\[ \mathbb{H}[Y, X - Y] = \mathbb{H}[X, Y] \]

(from Entropy and relabeling), and

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

(from Entropy and relabeling and Additivity of entropy) and rearranging, we indeed obtain (1).

Lean

Formalized as ent_of_diff_le.

Sources
Leanent_of_diff_le
Uses 4 · Used by 2
Proof usesAlternate form of submodularity · Subadditivity · Entropy and relabeling · Additivity of entropy
Used byRuzsa triangle inequality · Sums of dilates I

This is an improvement over the usual Ruzsa triangle inequality because \(X,Y\) are not assumed to be independent. However we will not utilize this improvement here.

The proof of Improved Ruzsa triangle inequality is shown with its statement.

LemmaRuzsa triangle inequality#

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

\[ d[X ;Y] \leq d[X ;Z] + d[Z;Y]. \]
Proof

By Copy preserves Ruzsa distance and Lemmas Existence of independent copies, Ruzsa distance in independent case, it suffices to prove this inequality assuming that \(X,Y,Z\) are defined on the same space and are independent. But then the claim follows from Improved Ruzsa triangle inequality and Ruzsa distance.

Lean

Formalized as rdist_triangle.

Sources
Leanrdist_triangle
Uses 4 · Used by 8
Proof usesCopy preserves Ruzsa distance · Ruzsa distance in independent case · Existence of independent copies · Improved Ruzsa triangle inequality
Used byEntropy version of PFR · Improved entropy version of PFR · General 100% inverse theorem · Bounding mutual information · Multidistance and Ruzsa distance, II · Lower bound on multidistance · Entropy form of PFR · torsion-free-doubling

DefinitionConditioned Ruzsa distance#

If \((X, Z)\) and \((Y, W)\) are random variables (where \(X\) and \(Y\) are \(G\)-valued) we define

\[ d[X | Z; Y | W] := \sum_{z,w} \mathbb{P}[Z=z] \mathbb{P}[W=w] d[(X|Z=z); (Y|(W=w))]. \]

similarly

\[ d[X ; Y | W] := \sum_{w} \mathbb{P}[W=w] d[X ; (Y|(W=w))]. \]
Lean

Formalized as condRuzsaDist.

Sources
LeancondRuzsaDist
Uses 1 · Used by 3
Statement usesRuzsa distance
Used byAlternate form of distance · Upper bound on conditioned Ruzsa distance · Conditional distance lower bound

LemmaAlternate form of distance#

The expression \(d[X | Z;Y | W]\) is unchanged if \((X,Z)\) or \((Y,W)\) is replaced by a copy. Furthermore, if \((X,Z)\) and \((Y,W)\) are independent, then

\[ d[X | Z;Y | W] = \mathbb{H}[X-Y|Z,W] - \mathbb{H}[X|Z]/2 - \mathbb{H}[Y|W]/2 \]

and similarly

\[ d[X ;Y | W] = \mathbb{H}[X-Y|W] - \mathbb{H}[X]/2 - \mathbb{H}[Y|W]/2. \]
Proof

Straightforward thanks to Copy preserves entropy, Copy preserves Ruzsa distance, Ruzsa distance in independent case, Conditioned Ruzsa distance, Conditional entropy.

Lean

Formalized as condRuzsaDist_of_copy, condRuzsaDist'_of_copy, condRuzsaDist_of_indep, condRuzsaDist'_of_indep.

Sources
LeancondRuzsaDist_of_copy · condRuzsaDist'_of_copy · condRuzsaDist_of_indep · condRuzsaDist'_of_indep
Uses 5 · Used by 2
Proof usesCopy preserves entropy · Copy preserves Ruzsa distance · Ruzsa distance in independent case · Conditioned Ruzsa distance · Conditional entropy
Used byUpper bound on conditioned Ruzsa distance · General fibring identity

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.