The tau functional

Fix \(m \geq 2\), and a reference variable \(X^0\) in \(G\).

Definition\(\eta\)#

We set \(\eta := \frac{1}{32m^3}\).

Lean

Formalized as multiRefPackage.

Sources
LeanmultiRefPackage
Used by 2
Used byVanishing entropy · Entropy form of PFR

Definition\(\tau\)-functional#

If \((X_i)_{1 \leq i \leq m}\) is a tuple, we define its \(\tau\)-functional

\[ \tau[ (X_i)_{1 \leq i \leq m}] := D[(X_i)_{1 \leq i \leq m}] + \eta \sum_{i=1}^m d[X_i; X^0]. \]
Lean

Formalized as multiTau.

Sources
LeanmultiTau
Uses 1 · Used by 2
Statement usesMultidistance
Used byExistence of \(\tau\)-minimizer · \(\tau\)-minimizer

Definition\(\tau\)-minimizer#

A \(\tau\)-minimizer is a tuple \((X_i)_{1 \leq i \leq m}\) that minimizes the \(\tau\)-functional among all tuples of \(G\)-valued random variables.

Lean

Formalized as multiTauMinimizes.

Sources
LeanmultiTauMinimizes
Uses 1 · Used by 2
Statement uses\(\tau\)-functional
Used byLower bound on multidistance · Minimizer close to reference variables

PropositionExistence of \(\tau\)-minimizer#

If \(G\) is finite, then a \(\tau\)-minimizer exists.

Proof

This is similar to the proof of \(\tau\) has minimum.

Lean

Formalized as multiTau_continuous, multiTau_min_exists.

Sources
LeanmultiTau_continuous · multiTau_min_exists
Uses 1 · Used by 1
Proof uses\(\tau\)-functional
Used byEntropy form of PFR

PropositionMinimizer close to reference variables#

If \((X_i)_{1 \leq i \leq m}\) is a \(\tau\)-minimizer, then \(\sum_{i=1}^m d[X_i; X^0] \leq \frac{2m}{\eta} d[X^0; X^0]\).

Proof

By \(\tau\)-minimizer we have

\[ \tau[ (X_i)_{1 \leq i \leq m}] \leq \tau[ (X^0)_{1 \leq i \leq m}] \]

and hence by \(\tau\)-functional and Nonnegativity

\[ \eta \sum_{i=1}^m d[X_i; X^0] \leq D[(X^0)_{1 \leq i \leq m}] + m d[X^0; X^0]. \]

The claim now follows from Multidistance and Ruzsa distance, III.

Lean

Formalized as multiTau_min_sum_le.

Sources
LeanmultiTau_min_sum_le
Uses 3 · Used by 1
Proof uses\(\tau\)-minimizer · Nonnegativity · Multidistance and Ruzsa distance, III
Used byEntropy form of PFR

LemmaLower bound on multidistance#

If \((X_i)_{1 \leq i \leq m}\) is a \(\tau\)-minimizer, and \(k := D[(X_i)_{1 \leq i \leq m}]\), then for any other tuple \((X'_i)_{1 \leq i \leq m}\), one has

\[ k - D[(X'_i)_{1 \leq i \leq m}] \leq \eta \sum_{i=1}^m d[X_i; X'_i]. \]
Proof

By \(\tau\)-minimizer we have

\[ \tau[ (X_i)_{1 \leq i \leq m}] \leq \tau[ (X'_i)_{1 \leq i \leq m}] \]

and hence by \(\tau\)-functional

\[ k + \eta \sum_{i=1}^m d[X_i; X^0] \leq D[(X'_i)_{1 \leq i \leq m}] + \eta \sum_{i=1}^m d[X'_i; X^0]. \]

On the other hand, by Ruzsa triangle inequality we have

\[ d[X'_i; X^0] \leq d[X_i; X^0] + d[X_i; X'_i]. \]

The claim follows.

Lean

Formalized as sub_multiDistance_le.

Sources
Leansub_multiDistance_le
Uses 2 · Used by 2
Proof uses\(\tau\)-minimizer · Ruzsa triangle inequality
Used byVanishing entropy · Lower bound on conditional multidistance

DefinitionConditional multidistance#

If \(X_{[m]} = (X_i)_{1 \leq i \leq m}\) and \(Y_{[m]} = (Y_i)_{1 \leq i \leq m}\) are tuples of random variables, with the \(X_i\) being \(G\)-valued (but the \(Y_i\) need not be), then we define

\[ D[ X_{[m]} | Y_{[m]} ] = \sum_{(y_i)_{1 \leq i \leq m}} \biggl(\prod_{1 \leq i \leq m} p_{Y_i}(y_i)\biggr) D[ (X_i \,|\, Y_i \mathop{=}y_i)_{1 \leq i \leq m}]\qquad\text{(1)} \]

where each \(y_i\) ranges over the support of \(p_{Y_i}\) for \(1 \leq i \leq m\).

Lean

Formalized as condMultiDist.

Sources
LeancondMultiDist
Uses 1 · Used by 3
Statement usesMultidistance
Used byAlternate form of conditional multidistance · Lower bound on conditional multidistance · Conditional multidistance nonnegative

LemmaAlternate form of conditional multidistance#

If the \((X_i,Y_i)\) are independent,

\[ D[ X_{[m]} | Y_{[m]}] := \mathbb{H}[\sum_{i=1}^m X_i \big| (Y_j)_{1 \leq j \leq m} ] - \frac{1}{m} \sum_{i=1}^m \mathbb{H}[ X_i | Y_i].\qquad\text{(2)} \]
Proof

This is routine from Conditional entropy and Definitions Multidistance and Conditional multidistance.

Lean

Formalized as condMultiDist_eq.

Sources
LeancondMultiDist_eq
Uses 3 · Used by 1
Proof usesConditional entropy · Multidistance · Conditional multidistance
Used byLower bound on conditional multidistance

LemmaConditional multidistance nonnegative#

If \(X_{[m]} = (X_i)_{1 \leq i \leq m}\) and \(Y_{[m]} = (Y_i)_{1 \leq i \leq m}\) are tuples of random variables, then \(D[ X_{[m]} | Y_{[m]} ] \geq 0\).

Proof

Clear from Nonnegativity and Conditional multidistance, except that some care may need to be taken to deal with the \(y_i\) where \(p_{Y_i}\) vanish.

Lean

Formalized as condMultiDist_nonneg.

Sources
LeancondMultiDist_nonneg
Uses 2
Statement usesConditional multidistance
Proof usesNonnegativity

LemmaLower bound on conditional multidistance#

If \((X_i)_{1 \leq i \leq m}\) is a \(\tau\)-minimizer, and \(k := D[(X_i)_{1 \leq i \leq m}]\), then for any other tuples \((X'_i)_{1 \leq i \leq m}\) and \((Y_i)_{1 \leq i \leq m}\) with the \(X'_i\) \(G\)-valued, one has

\[ k - D[(X'_i)_{1 \leq i \leq m} | (Y_i)_{1 \leq i \leq m}] \leq \eta \sum_{i=1}^m d[X_i; X'_i|Y_i]. \]
Proof

Immediate from Lower bound on multidistance, Alternate form of conditional multidistance, and Conditioned Ruzsa distance.

Lean

Formalized as sub_condMultiDistance_le.

Sources
Leansub_condMultiDistance_le
Uses 3 · Used by 1
Proof usesLower bound on multidistance · Conditional multidistance · Alternate form of conditional multidistance
Used byLower bound on conditional multidistance, II

CorollaryLower bound on conditional multidistance, II#

With the notation of the previous lemma, we have

\[ k - D[ X'_{[m]} | Y_{[m]} ] \leq \eta \sum_{i=1}^m d[X_{\sigma(i)};X'_i|Y_i]\qquad\text{(3)} \]

for any permutation \(\sigma : \{1,\dots,m\} \rightarrow \{1,\dots,m\}\).

Proof

This follows from Lower bound on conditional multidistance and Relabeling.

Lean

Formalized as sub_condMultiDistance_le'.

Sources
Leansub_condMultiDistance_le'
Uses 2 · Used by 1
Proof usesLower bound on conditional multidistance · Relabeling
Used byBounding mutual information

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.