Rho functionals

Let \(G\) be an additive group, and let \(A\) be a non-empty subset of \(G\).

DefinitionRho minus#

For any \(G\)-valued random variable \(X\), we define \(\rho^-(X)\) to be the infimum of \(D_{KL}(X \Vert U_A + T)\), where \(U_A\) is uniform on \(A\) and \(T\) ranges over \(G\)-valued random variables independent of \(U_A\).

Lean

Formalized as rhoMinus.

Sources
LeanrhoMinus
Used by 2
Used byRho minus of subgroup · Rho plus

DefinitionRho plus#

For any \(G\)-valued random variable \(X\), we define \(\rho^+(X) := \rho^-(X) + \mathbb{H}(X) - \mathbb{H}(U_A)\).

Lean

Formalized as rhoPlus.

Sources
LeanrhoPlus
Uses 1 · Used by 2
Statement usesRho minus
Used byRho functional · Rho plus of subgroup

LemmaRho minus of subgroup#

If \(H\) is a finite subgroup of \(G\), then \(\rho^-(U_H) = \log |A| - \log \max_t |A \cap (H+t)|\).

Proof

For every \(G\)-valued random variable \(T\) that is independent of \(Y\),

\[ D_{KL}(U_H \Vert U_A+T) = \sum_{h\in H} \frac{1}{|H|}\log\frac{1/|H|}{\mathbf{P}[U_A+T=h]}\ge -\log(\mathbf{P}[U_A+T\in H]), \]

by log sum inequality. Then observe that

\[ -\log(\mathbf{P}[U_A+T\in H])=-\log(\mathbf{P}[U_A\in H-T])\ge -\log(\max_{t\in G} \mathbf{P}[U_A\in H+t]). \]

This proves \(\ge\).

To get the equality, let \(t^*:=\arg\max_t |A \cap (H+t)|\) and observe that

\[ \rho^-(U_H)\le D_{KL}(U_H \Vert U_A+(U_H-t^*))= \log |A| - \log \max_t|A \cap (H+t)|. \]
Lean

Formalized as rhoMinus_of_subgroup.

Sources
LeanrhoMinus_of_subgroup
Uses 2 · Used by 2
Statement usesRho minus
Proof useslog sum inequality
Used byRho of subgroup · Rho plus of subgroup

CorollaryRho plus of subgroup#

If \(H\) is a finite subgroup of \(G\), then \(\rho^+(U_H) = \log |H| - \log \max_t |A \cap (H+t)|\).

Proof

Straightforward by definition and Rho minus of subgroup.

Lean

Formalized as rhoPlus_of_subgroup.

Sources
LeanrhoPlus_of_subgroup
Uses 2 · Used by 1
Statement usesRho plus
Proof usesRho minus of subgroup
Used byRho of subgroup

DefinitionRho functional#

We define \(\rho(X) := (\rho^+(X) + \rho^-(X))/2\).

Lean

Formalized as rho.

Sources
Leanrho
Uses 1 · Used by 3
Statement usesRho plus
Used byRho continuous · Rho invariant · Rho of subgroup

LemmaRho of subgroup#

If \(H\) is a finite subgroup of \(G\), and \(\rho(U_H) \leq r\), then there exists \(t\) such that \(|A \cap (H+t)| \geq e^{-r} \sqrt{|A||H|}\), and \(|H|/|A|\in[e^{-2r},e^{2r}]\).

Proof

The first claim is a direct corollary of Rho minus of subgroup and Rho plus of subgroup. To see the second claim, observe that Rho minus non-negative and Rho plus of subgroup imply \(\rho^-(U_H),\rho^+(U_H)\ge 0\). Therefore

\[ |H(U_A)-H(U_H)|=|\rho^+(U_H)-\rho^-(U_H)|\le \rho^-(U_H)+\rho^+(U_H)= 2\rho(U_H)\le 2r, \]

which implies the second claim.

Lean

Formalized as rho_of_subgroup.

Sources
Leanrho_of_subgroup
Uses 3 · Used by 1
Statement usesRho functional
Proof usesRho minus of subgroup · Rho plus of subgroup
Used bypfr-9-aux

LemmaRho invariant#

For any \(s \in G\), \(\rho(X+s) = \rho(X)\).

Proof

Observe that by Kullback–Leibler and injections,

\[ \inf_T D_{KL}(X\Vert U_A+T)=\inf_T D_{KL}(X+s\Vert U_A+T+s)=\inf_{T'} D_{KL}(X+s\Vert U_A+T'). \]
Lean

Formalized as rho_of_translate.

Sources
Leanrho_of_translate
Uses 2 · Used by 3
Statement usesRho functional
Proof usesKullback–Leibler and injections
Used byConditional rho and translation · Rho and conditioning, symmetrized · pfr-rho

LemmaRho continuous#

\(\rho(X)\) depends continuously on the distribution of \(X\).

Proof

Clear from definition.

Lean

Formalized as rho_continuous.

Sources
Leanrho_continuous
Uses 1 · Used by 1
Statement usesRho functional
Used by\(\phi\)-minimizers exist

LemmaRho and sums#

If \(X,Y\) are independent, one has

\[ \rho^-(X+Y) \leq \rho^-(X) \]
\[ \rho^+(X+Y) \leq \rho^+(X) + \mathbb{H}[X+Y] - \mathbb{H}[X] \]

and

\[ \rho(X+Y) \leq \rho(X) + \frac{1}{2}( \mathbb{H}[X+Y] - \mathbb{H}[X] ). \]
Proof

The first inequality follows from Kullback–Leibler and sums. The second and third inequalities are direct corollaries of the first.

Lean

Formalized as rhoMinus_of_sum, rhoPlus_of_sum, rho_of_sum.

Sources
LeanrhoMinus_of_sum · rhoPlus_of_sum · rho_of_sum
Uses 1 · Used by 1
Proof usesKullback–Leibler and sums
Used byRho and sums, symmetrized

DefinitionConditional Rho functional#

We define \(\rho(X|Y) := \sum_y {\bf P}(Y=y) \rho(X|Y=y)\).

Lean

Formalized as condRho.

Sources
LeancondRho
Used by 2
Used byConditional rho and translation · Conditional rho and relabeling

LemmaConditional rho and translation#

For any \(s\in G\), \(\rho(X+s|Y)=\rho(X|Y)\).

Proof

Direct corollary of Rho invariant.

Lean

Formalized as condRho_of_translate.

Sources
LeancondRho_of_translate
Uses 2
Proof usesConditional Rho functional · Rho invariant

LemmaConditional rho and relabeling#

If \(f\) is injective, then \(\rho(X|f(Y))=\rho(X|Y)\).

Proof

Clear from the definition.

Lean

Formalized as condRho_of_injective.

Sources
LeancondRho_of_injective
Uses 1 · Used by 1
Proof usesConditional Rho functional
Used byrho-increase

LemmaRho and conditioning#

If \(X,Z\) are defined on the same space, one has

\[ \rho^-(X|Z) \leq \rho^-(X) + \mathbb{H}[X] - \mathbb{H}[X|Z] \]
\[ \rho^+(X|Z) \leq \rho^+(X) \]

and

\[ \rho(X|Z) \leq \rho(X) + \frac{1}{2}( \mathbb{H}[X] - \mathbb{H}[X|Z] ). \]
Proof

The first inequality follows from Kullback–Leibler and conditioning. The second and third inequalities are direct corollaries of the first.

Lean

Formalized as condRhoMinus_le, condRhoPlus_le, condRho_le.

Sources
LeancondRhoMinus_le · condRhoPlus_le · condRho_le
Uses 1 · Used by 2
Proof usesKullback–Leibler and conditioning
Used byRho and conditioning, symmetrized · rho-increase

The following lemmas hold for \(G=\mathbb{F}_2^n\).

LemmaRho and sums, symmetrized#

If \(X,Y\) are independent, then

\[ \rho(X+Y) \leq \frac{1}{2}(\rho(X)+\rho(Y) + d[X;Y]). \]
Proof

Apply Rho and sums for \((X,Y)\) and \((Y,X)\) and take their average.

Lean

Formalized as rho_of_sum_le.

Sources
Leanrho_of_sum_le
Uses 1 · Used by 1
Proof usesRho and sums
Used byrho-increase

LemmaRho and conditioning, symmetrized#

If \(X,Y\) are independent, then

\[ \rho(X | X+Y) \leq \frac{1}{2}(\rho(X)+\rho(Y) + d[X;Y]). \]
Proof

First apply Rho and conditioning to get \(\rho(X|X+Y)\le \rho(X) + \frac{1}{2}(\mathbb{H}[X+Y]-\mathbb{H}[Y])\), and \(\rho(Y|X+Y)\le \rho(Y)+\frac{1}{2}(\mathbb{H}[X+Y]-\mathbb{H}[X])\). Then apply Rho invariant to get \(\rho(Y|X+Y)=\rho(X|X+Y)\) and take the average of the two inequalities.

Lean

Formalized as condRho_of_sum_le.

Sources
LeancondRho_of_sum_le
Uses 2 · Used by 1
Proof usesRho invariant · Rho and conditioning
Used byrho-increase

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.