Entropy version of PFR

Throughout this chapter, \(G = \mathbb{F}_2^n\), and \(X^0_1, X^0_2\) are \(G\)-valued random variables.

Definition\(\tau\) functional#

If \(X_1,X_2\) are two \(G\)-valued random variables, then

\[ \tau[X_1; X_2] := d[X_1; X_2] + \eta d[X^0_1; X_1] + \eta d[X^0_2; X_2]. \]
Lean

Formalized as tau.

Sources
Leantau
Uses 1 · Used by 4
Statement usesRuzsa distance
Used byDistance lower bound · \(\tau\) depends only on distribution · \(\tau\)-minimizer · Entropy form of PFR

Lemma\(\tau\) depends only on distribution#

If \(X'_1, X'_2\) are copies of \(X_1,X_2\), then \(\tau[X'_1;X'_2] = \tau[X_1;X_2]\).

Proof

Immediate from Copy preserves entropy.

Lean

Formalized as ProbabilityTheory.IdentDistrib.tau_eq.

Sources
LeanProbabilityTheory.IdentDistrib.tau_eq
Uses 2 · Used by 1
Statement uses\(\tau\) functional
Proof usesCopy preserves entropy
Used by\(\tau\) has minimum

Definition\(\tau\)-minimizer#

A pair of \(G\)-valued random variables \(X_1, X_2\) are said to be a \(\tau\)-minimizer if one has

\[ \tau[X_1;X_2] \leq \tau[X'_1;X'_2] \]

for all \(G\)-valued random variables \(X'_1, X'_2\).

Lean

Formalized as TauMinimizes.

Sources
LeanTauMinimizes
Uses 1 · Used by 3
Statement uses\(\tau\) functional
Used byConditional distance lower bound · Distance lower bound · \(\tau\) has minimum

Proposition\(\tau\) has minimum#

A pair \(X_1, X_2\) of \(\tau\)-minimizers exist.

Proof

By \(\tau\) depends only on distribution, \(\tau\) only depends on the probability distributions of \(X_1, X_2\). This ranges over a compact space, and \(\tau\) is continuous. So \(\tau\) has a minimum.

Lean

Formalized as tau_minimizer_exists.

Sources
Leantau_minimizer_exists
Uses 2 · Used by 3
Statement uses\(\tau\)-minimizer
Proof uses\(\tau\) depends only on distribution
Used byDistance lower bound · Entropy version of PFR · Limiting improved \(\tau\)-decrement

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.