Dependency graph

Legend

Boxes: definitions
Ellipses: theorems and lemmas
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Orange border: the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background: the proof of this result is ready to be formalized; all prerequisites are done
Green border: the statement of this result is formalized
Green background: the proof of this result is formalized
Dark green background: the proof of this result and all its ancestors are formalized

Corollary 2.24Additivity of entropy

If $X, Y$ are random variables, then $H [X, Y] = H [X] + H [Y]$ if and only if $X, Y$ are independent.

LaTeX Lean

Corollary 2.21Alternate form of submodularity

With three random variables $X, Y, Z$ , one has

H [X, Y, Z] + H [Z] \leq H [X, Z] + H [Y, Z] .

LaTeX Lean

Lemma 2.16Alternative formulae for mutual information

With notation as above, we have

I [X : Y] = I [Y : X]

I [X : Y] = H [X] - H [X | Y]

I [X : Y] = H [Y] - H [Y | X]

LaTeX

Lean

ProbabilityTheory.mutualInfo_comm
ProbabilityTheory.mutualInfo_eq_entropy_sub_condEntropy

Lemma 11.3

Let $G = F_{2}^{n}$ and $α \in (0, 1)$ and let $X, Y$ be $G$ -valued random variables such that

H (X) + H (Y) > \frac{20}{α} d [X; Y] .

There is a non-trivial subgroup $H \leq G$ such that

\log | H | < \frac{1 + α}{2} (H (X) + H (Y))

and

H (ψ (X)) + H (ψ (Y)) < α (H (X) + H (Y))

where $ψ : G \to G / H$ is the natural projection homomorphism.

LaTeX Lean

Theorem 10.4Approximate homomorphism form of PFR

Let $G, G^{'}$ be finite abelian $2$ -groups. Let $f : G \to G^{'}$ be a function, and suppose that there are at least $| G |^{2} / K$ pairs $(x, y) \in G^{2}$ such that

f (x + y) = f (x) + f (y) .

Then there exists a homomorphism $ϕ : G \to G^{'}$ and a constant $c \in G^{'}$ such that $f (x) = ϕ (x) + c$ for at least $| G | / (2^{144} * K^{122})$ values of $x \in G$ .

LaTeX Lean

Lemma 8.4Constructing good variables, III’

One has

\begin{aligned} k & \leq I (U : V | S) + I (V : W | S) + I (W : U | S) + \frac{η}{6} \sum_{i = 1}^{2} \sum_{A, B \in {U, V, W} : A \neq B} (d [X_{i}^{0}; A | B, S] - d [X_{i}^{0}; X_{i}]) . \end{aligned}

LaTeX Lean

Lemma 2.8Bounded entropy implies concentration

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

LaTeX Lean

Lemma 10.3Balog–Szemerédi–Gowers lemma

Let $G$ be an abelian group, and let $A$ be a finite non-empty set with $E (A) \geq | A |^{3} / K$ for some $K \geq 1$ . Then there is a subset $A^{'}$ of $A$ with $| A^{'} | \geq | A | / (C_{1} K^{C_{2}})$ and $| A^{'} - A^{'} | \leq C_{3} K^{C_{4}} | A |$ , where (provisionally)

C_{1} = 2^{4}, C_{2} = 1, C_{3} = 2^{10}, C_{4} = 5.

LaTeX Lean

Lemma 2.13Chain rule

If $X : Ω \to S$ and $Y : Ω \to T$ are random variables, then

H [X, Y] = H [Y] + H [X | Y] .

LaTeX

Lean

ProbabilityTheory.chain_rule
ProbabilityTheory.chain_rule'

Definition 13.8Conditional Kullback–Leibler divergence

If $X, Y, Z$ are random variables, with $X, Z$ defined on the same sample space, we define

D_{K L} (X | Z ‖ Y) := \sum_{z} P (Z = z) D_{K L} ((X | Z = z) ‖ Y) .

LaTeX

Lemma 12.9Comparing sums

Let $(X_{i})_{1 \leq i \leq m}$ and $(Y_{j})_{1 \leq j \leq l}$ be tuples of jointly independent random variables (so the $X$ ’s and $Y$ ’s are also independent of each other), and let $f : {1, \dots, l} \to {1, \dots, m}$ be a function, then

H [\sum_{j = 1}^{l} Y_{j}] \leq H [\sum_{i = 1}^{m} X_{i}] + \sum_{j = 1}^{l} (H [Y_{j} - X_{f (j)}] - H [X_{f (j)}]) .

LaTeX Lean

Lemma 1.1Concavity

$h$ is strictly concave on $[0, \infty)$ .

LaTeX Lean

Lemma 3.20Alternate 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] = H [X - Y | Z, W] - H [X | Z] / 2 - H [Y | W] / 2

and similarly

d [X; Y | W] = H [X - Y | W] - H [X] / 2 - H [Y | W] / 2.

LaTeX

Lean

condRuzsaDist_of_copy
condRuzsaDist'_of_copy
condRuzsaDist_of_indep
condRuzsaDist'_of_indep

Definition 3.19Conditioned 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} P [Z = z] P [W = w] d [(X | Z = z); (Y | (W = w))] .

similarly

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

LaTeX Lean

Lemma 3.24Upper bound on conditioned Ruzsa distance

Suppose that $(X, Z)$ and $(Y, W)$ are random variables, where $X, Y$ take values in an abelian group. Then

d [X | Z; Y | W] \leq d [X; Y] + \frac{1}{2} I [X : Z] + \frac{1}{2} I [Y : W] .

In particular,

d [X; Y | W] \leq d [X; Y] + \frac{1}{2} I [Y : W] .

LaTeX

Lean

condRuzsaDist_le
condRuzsaDist_le'

Lemma 6.7Conditional distance lower bound

For any $G$ -valued random variables $X_{1}^{'}, X_{2}^{'}$ and random variables $Z, W$ , one has

d [X_{1}^{'} | Z; X_{2}^{'} | W] \geq k - η (d [X_{1}^{0}; X_{1}^{'} | Z] - d [X_{1}^{0}; X_{1}]) - η (d [X_{2}^{0}; X_{2}^{'} | W] - d [X_{2}^{0}; X_{2}]) .

LaTeX Lean

Lemma 3.22Existence of conditional independent trials

For $X, Y$ random variables, there exist random variables $X_{1}, X_{2}, Y^{'}$ on a common probability space with $(X_{1}, Y^{'}), (X_{2}, Y^{'})$ both having the distribution of $(X, Y)$ , and $X_{1}, X_{2}$ conditionally independent over $Y^{'}$ in the sense of Definition 2.28.

LaTeX Lean

Lemma 12.29Alternate form of conditional multidistance

If the $(X_{i}, Y_{i})$ are independent,

D [X_{[m]} | Y_{[m]}] := H [\sum_{i = 1}^{m} X_{i} | (Y_{j})_{1 \leq j \leq m}] - \frac{1}{m} \sum_{i = 1}^{m} H [X_{i} | Y_{i}] .

LaTeX Lean

Definition 12.28Conditional 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}} (\prod_{1 \leq i \leq m} p_{Y_{i}} (y_{i})) D [(X_{i} | Y_{i} = y_{i})_{1 \leq i \leq m}]

where each $y_{i}$ ranges over the support of $p_{Y_{i}}$ for $1 \leq i \leq m$ .

LaTeX Lean

Lemma 12.31Lower bound on conditional multidistance

If $(X_{i})_{1 \leq i \leq m}$ is a $τ$ -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 η \sum_{i = 1}^{m} d [X_{i}; X_{i}^{'} | Y_{i}] .

LaTeX Lean

Corollary 12.32Lower bound on conditional multidistance, II

With the notation of the previous lemma, we have

k - D [X_{[m]}^{'} | Y_{[m]}] \leq η \sum_{i = 1}^{m} d [X_{σ (i)}; X_{i}^{'} | Y_{i}]

for any permutation $σ : {1, \dots, m} \to {1, \dots, m}$ .

LaTeX Lean

Lemma 12.30Conditional 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$ .

LaTeX Lean

Corollary 2.19Conditioning reduces entropy

With notation as above, we have $H [X | Y] \leq H [X]$ .

LaTeX Lean

Corollary 2.30Entropy of conditionally independent variables

If $X, Y$ are conditionally independent over $Z$ , then

H [X, Y, Z] = H [X, Z] + H [Y, Z] - H [Z] .

LaTeX Lean

Definition 2.10Conditioned event

If $X : Ω \to S$ is an $S$ -valued random variable and $E$ is an event in $Ω$ , 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$ .

LaTeX Lean

Lemma 2.14Conditional chain rule

If $X : Ω \to S$ , $Y : Ω \to T$ , $Z : Ω \to U$ are random variables, then

H [X, Y | Z] = H [Y | Z] + H [X | Y, Z] .

LaTeX

Lean

ProbabilityTheory.cond_chain_rule
ProbabilityTheory.cond_chain_rule'

Definition 2.11Conditional entropy

If $X : Ω \to S$ and $Y : Ω \to T$ are random variables, the conditional entropy $H [X | Y]$ is defined as

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

LaTeX Lean

Lemma 13.10Conditional Gibbs inequality

$D_{K L} ((X | W) ‖ Y) \geq 0$ .

LaTeX Lean

Definition 2.28Conditionally independent random variables

Two random variables $X : Ω \to S$ and $Y : Ω \to T$ are conditionally independent relative to another random variable $Z : Ω \to U$ if $P [X = s \land Y = t | Z = u] = P [X = s | Z = u] P [Y = t | Z = u]$ for all $s \in S, t \in T, u \in U$ . (We won’t need conditional independence for more variables than this.)

LaTeX Lean

Lemma 2.26Alternate formula for conditional mutual information

We have

I [X : Y | Z] := H [X | Z] + H [Y | Z] - H [X, Y | Z]

and

I [X : Y | Z] := H [X | Z] - H [X | Y, Z] .

LaTeX

Lean

ProbabilityTheory.condMutualInfo_eq
ProbabilityTheory.condMutualInfo_eq'

Definition 2.25Conditional mutual information

If $X, Y, Z$ are random variables, with $Z$ $U$ -valued, then

I [X : Y | Z] := \sum_{z \in U} P [Z = z] I [(X | Z = z) : (Y | Z = z)] .

LaTeX Lean

Lemma 2.27Nonnegativity of conditional mutual information

If $X, Y, Z$ are random variables, then $I [X : Y | Z] \geq 0$ .

LaTeX Lean

Lemma 2.29Vanishing conditional mutual information

If $X, Y, Z$ are random variables, then $I [X : Y | Z] = 0$ iff $X, Y$ are conditionally independent over $Z$ .

LaTeX Lean

Lemma 6.22Constructing good variables, II

One has

\begin{aligned} k & \leq δ + \frac{η}{3} (δ + \sum_{i = 1}^{2} \sum_{j = 1}^{3} (d [X_{i}^{0}; T_{j}] - d [X_{i}^{0}; X_{i}])) . \end{aligned}

LaTeX Lean

Lemma 8.3Constructing good variables, II’

One has

\begin{aligned} k & \leq δ + \frac{η}{6} \sum_{i = 1}^{2} \sum_{1 \leq j, l \leq 3; j \neq l} (d [X_{i}^{0}; T_{j} | T_{l}] - d [X_{i}^{0}; X_{i}]) \end{aligned}

LaTeX Lean

Lemma 6.21Constructing good variables, I

One has

\begin{aligned} k \leq δ + η ( & d [X_{1}^{0}; T_{1}] - d [X_{1}^{0}; X_{1}]) + η (d [X_{2}^{0}; T_{2}] - d [X_{2}^{0}; X_{2}]) \\ + \frac{1}{2} η I [T_{1} : T_{3}] + \frac{1}{2} η I [T_{2} : T_{3}] . \end{aligned}

LaTeX Lean

Lemma 8.2Constructing good variables, I’

One has

\begin{aligned} k \leq δ + η ( & d [X_{1}^{0}; T_{1} | T_{3}] - d [X_{1}^{0}; X_{1}]) + η (d [X_{2}^{0}; T_{2} | T_{3}] - d [X_{2}^{0}; X_{2}]) . \end{aligned}

LaTeX Lean

Lemma 1.3Converse Jensen

If equality holds in the above lemma, then $p_{s} = \sum_{s \in S} w_{s} h (p_{s})$ whenever $w_{s} \neq 0$ .

LaTeX Lean

Lemma 1.5converse log sum

If equality holds in Lemma 1.4, then $a_{s} = r \cdot b_{s}$ for every $s \in S$ , for some constant $r \in R$ .

LaTeX Lean

Lemma 3.6Copy preserves entropy

If $X^{'}$ is a copy of $X$ then $H [X^{'}] = H [X]$ .

LaTeX Lean

Corollary 5.3Specific fibring identity

Let $Y_{1}, Y_{2}, Y_{3}$ and $Y_{4}$ be independent $G$ -valued random variables. Then

\begin{aligned} d [Y_{1} + Y_{3}; Y_{2} + Y_{4}] + d [Y_{1} | Y_{1} + Y_{3}; Y_{2} | Y_{2} + Y_{4}] \\ + I [Y_{1} + Y_{2} : Y_{2} + Y_{4} | Y_{1} + Y_{2} + Y_{3} + Y_{4}] = d [Y_{1}; Y_{2}] + d [Y_{3}; Y_{4}] . \end{aligned}

LaTeX Lean

Corollary 12.36

Let $G$ be an abelian group and let $m \geq 2$ . Suppose that $X_{i, j}$ , $1 \leq i, j \leq m$ , are independent $G$ -valued random variables. Then

\begin{aligned} I [(\sum_{i = 1}^{m} X_{i, j})_{j = 1}^{m} : (\sum_{j = 1}^{m} X_{i, j})_{i = 1}^{m} | \sum_{i = 1}^{m} \sum_{j = 1}^{m} X_{i, j}] \\ \leq \sum_{j = 1}^{m - 1} (D [(X_{i, j})_{i = 1}^{m}] - D [(X_{i, j})_{i = 1}^{m} | (X_{i, j} + \dots + X_{i, m})_{i = 1}^{m}]) \\ + D [(X_{i, m})_{i = 1}^{m}] - D [(\sum_{j = 1}^{m} X_{i, j})_{i = 1}^{m}], \end{aligned}

where all the multidistances here involve the indexing set ${1, \dots, m}$ .

LaTeX Lean

Lemma 10.2Cauchy–Schwarz bound

If $G$ is a group, $A, B$ are finite subsets of $G$ , then

E (A) \geq \frac{| {(a, a^{'}) \in A \times A : a + a^{'} \in B} |^{2}}{| B |} .

LaTeX Lean

Lemma 12.4Data processing inequality

Let $X, Y, Z$ . For any functions $f, g$ on the ranges of $X, Y$ respectively, we have $I [f (X) : g (Y) | Z] \leq I [X : Y | Z]$ .

LaTeX Lean

Lemma 12.1Data processing for a single variable

Let $X$ be a random variable. Then for any function $f$ on the range of $X$ , one has $H [f (X)] \leq H [X]$ .

LaTeX Lean

Lemma 12.3Unconditional data processing inequality

Let $X, Y$ be random variables. For any functions $f, g$ on the ranges of $X, Y$ respectively, we have $I [f (X) : g (Y)] \leq I [X : Y]$ .

LaTeX Lean

Lemma 12.2One-sided unconditional data processing inequality

Let $X, Y$ be random variables. For any function $f, g$ on the range of $X$ , we have $I [f (X) : Y] \leq I [X : Y]$ .

LaTeX Lean

Theorem 6.23

τ

-decrement

Let $X_{1}, X_{2}$ be tau-minimizers. Then $d [X_{1}; X_{2}] = 0$ .

LaTeX Lean

Theorem 8.7Improved

τ

-decrement

Suppose $0 < η < 1 / 8$ . Let $X_{1}, X_{2}$ be tau-minimizers. Then $d [X_{1}; X_{2}] = 0$ .

LaTeX Lean

Theorem 8.8Limiting improved

τ

-decrement

For $η = 1 / 8$ , there exist tau-minimizers $X_{1}, X_{2}$ satisfying $d [X_{1}; X_{2}] = 0$ .

LaTeX Lean

Definition 11.7

If $A \subseteq Z^{d}$ then by $\dim (A)$ we mean the dimension of the span of $A - A$ over the reals – equivalently, the smallest $d^{'}$ such that $A$ lies in a coset of a subgroup isomorphic to $Z^{d^{'}}$ .

LaTeX Lean

Lemma 8.6Bound on distance differences

We have

\begin{aligned} \sum_{i = 1}^{2} \sum_{A, B \in {U, V, W} : A \neq B} d [X_{i}^{0}; A | B, S] - d [X_{i}^{0}; X_{i}] \\ \leq 12 k + \frac{4 (2 η k - I_{1})}{1 - η} . \end{aligned}

LaTeX

Lean

dist_diff_bound_1
dist_diff_bound_2

Lemma 3.16Projection 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 $π : G \to G / H$ the natural homomorphism we have (where $U_{H}$ is uniform on $H$ )

H (π (X)) \leq 2 d [X; U_{H}] .

LaTeX Lean

Lemma 6.14Distance between sums

We have

d [X_{1} + {\tilde{X}}_{1}; X_{2} + {\tilde{X}}_{2}] \geq k - \frac{η}{2} (d [X_{1}; X_{1}] + d [X_{2}; X_{2}]) .

LaTeX Lean

Lemma 3.9Distance 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] = H (X) / 2.

LaTeX Lean

Lemma 6.6Distance lower bound

For any $G$ -valued random variables $X_{1}^{'}, X_{2}^{'}$ , one has

d [X_{1}^{'}; X_{2}^{'}] \geq k - η (d [X_{1}^{0}; X_{1}^{'}] - d [X_{1}^{0}; X_{1}]) - η (d [X_{2}^{0}; X_{2}^{'}] - d [X_{2}^{0}; X_{2}]) .

LaTeX Lean

Definition 10.1Additive energy

If $G$ is a group, and $A$ is a finite subset of $G$ , the additive energy $E (A)$ of $A$ is the number of quadruples $(a_{1}, a_{2}, a_{3}, a_{4}) \in A^{4}$ such that $a_{1} + a_{2} = a_{3} + a_{4}$ .

LaTeX Lean

Lemma 12.41Entropy of

W

We have $H [W] \leq (2 m - 1) k + \frac{1}{m} \sum_{i = 1}^{m} H [X_{i}]$ .

LaTeX Lean

Lemma 12.42Entropy of

Z_{2}

We have $H [Z_{2}] \leq (8 m^{2} - 16 m + 1) k + \frac{1}{m} \sum_{i = 1}^{m} H [X_{i}]$ .

LaTeX Lean

Lemma 3.23Balog-Szemerédi-Gowers

Let $A, B$ be $G$ -valued random variables on $Ω$ , and set $Z := A + B$ . Then

\sum_{z} P [Z = z] d [(A | Z = z); (B | Z = z)] \leq 3 I [A : B] + 2 H [Z] - H [A] - H [B] .

LaTeX Lean

Lemma 2.9Commutativity and associativity of joint entropy

If $X : Ω \to S$ , $Y : Ω \to T$ , and $Z : Ω \to U$ are random variables, then $H [X, Y] = H [Y, X]$ and $H [X, (Y, Z)] = H [(X, Y), Z]$ .

LaTeX

Lean

ProbabilityTheory.entropy_comm
ProbabilityTheory.entropy_assoc

Definition 2.1Entropy

If $X$ is an $S$ -valued random variable, the entropy $H [X]$ of $X$ is defined

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

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

LaTeX Lean

Theorem 6.24Entropy version of PFR

Let $G = F_{2}^{n}$ , and suppose that $X_{1}^{0}, X_{2}^{0}$ are $G$ -valued random variables. Then there is some subgroup $H \leq G$ such that

d [X_{1}^{0}; U_{H}] + d [X_{2}^{0}; U_{H}] \leq 11 d [X_{1}^{0}; X_{2}^{0}],

where $U_{H}$ is uniformly distributed on $H$ . Furthermore, both $d [X_{1}^{0}; U_{H}]$ and $d [X_{2}^{0}; U_{H}]$ are at most $6 d [X_{1}^{0}; X_{2}^{0}]$ .

LaTeX Lean

Theorem 8.9Improved entropy version of PFR

Let $G = F_{2}^{n}$ , and suppose that $X_{1}^{0}, X_{2}^{0}$ are $G$ -valued random variables. Then there is some subgroup $H \leq G$ such that

d [X_{1}^{0}; U_{H}] + d [X_{2}^{0}; U_{H}] \leq 10 d [X_{1}^{0}; X_{2}^{0}],

where $U_{H}$ is uniformly distributed on $H$ . Furthermore, both $d [X_{1}^{0}; U_{H}]$ and $d [X_{2}^{0}; U_{H}]$ are at most $6 d [X_{1}^{0}; X_{2}^{0}]$ .

LaTeX Lean

Definition 6.1

$η := 1 / 9$ .

LaTeX

Definition 12.22

η

We set $η := \frac{1}{32 m^{3}}$ .

LaTeX Lean

Definition 8.1New definition of

η

$η$ is a real parameter with $η > 0$ .

LaTeX

Proposition 5.1General fibring identity

Let $π : H \to H^{'}$ be a homomorphism additive groups, and let $Z_{1}, Z_{2}$ be $H$ -valued random variables. Then we have

d [Z_{1}; Z_{2}] \geq d [π (Z_{1}); π (Z_{2})] + d [Z_{1} | π (Z_{1}); Z_{2} | π (Z_{2})] .

Moreover, if $Z_{1}, Z_{2}$ are taken to be independent, then the difference between the two sides is

I (Z_{1} - Z_{2} : (π (Z_{1}), π (Z_{2})) | π (Z_{1} - Z_{2})) .

LaTeX

Lean

rdist_of_indep_eq_sum_fibre
rdist_le_sum_fibre

Corollary 5.2

If $π : G \to H$ is a homomorphism of additive groups and $X, Y$ are $G$ -valued random variables then

d [X; Y] \geq d [π (X); π (Y)] .

LaTeX Lean

Lemma 6.10Lower bound on conditional distances

We have

\begin{aligned} d [X_{1} | X_{1} + {\tilde{X}}_{2}; X_{2} | X_{2} + {\tilde{X}}_{1}] \\ \geq k - η (d [X_{1}^{0}; X_{1} | X_{1} + {\tilde{X}}_{2}] - d [X_{1}^{0}; X_{1}]) \\ - η (d [X_{2}^{0}; X_{2} | X_{2} + {\tilde{X}}_{1}] - d [X_{2}^{0}; X_{2}]) . \end{aligned}

LaTeX Lean

Lemma 6.9Lower bound on distances

We have

\begin{aligned} d [X_{1} + {\tilde{X}}_{2}; X_{2} + {\tilde{X}}_{1}] \geq k & - η (d [X_{1}^{0}; X_{1} + {\tilde{X}}_{2}] - d [X_{1}^{0}; X_{1}]) \\ - η (d [X_{2}^{0}; X_{2} + {\tilde{X}}_{1}] - d [X_{2}^{0}; X_{2}]) \end{aligned}

LaTeX Lean

Lemma 6.12First estimate

We have $I_{1} \leq 2 η k$ .

LaTeX Lean

Lemma 6.8Fibring identity for first estimate

We have

\begin{aligned} d [X_{1} + {\tilde{X}}_{2}; X_{2} + {\tilde{X}}_{1}] + d [X_{1} | X_{1} + {\tilde{X}}_{2}; X_{2} | X_{2} + {\tilde{X}}_{1}] \\ + I [X_{1} + X_{2} : {\tilde{X}}_{1} + X_{2} | X_{1} + X_{2} + {\tilde{X}}_{1} + {\tilde{X}}_{2}] = 2 k . \end{aligned}

LaTeX Lean

Lemma 6.11Upper bound on distance differences

We have

\begin{aligned} d [X_{1}^{0}; X_{1} + {\tilde{X}}_{2}] - d [X_{1}^{0}; X_{1}] & \leq \frac{1}{2} k + \frac{1}{4} H [X_{2}] - \frac{1}{4} H [X_{1}] \\ d [X_{2}^{0}; X_{2} + {\tilde{X}}_{1}] - d [X_{2}^{0}; X_{2}] & \leq \frac{1}{2} k + \frac{1}{4} H [X_{1}] - \frac{1}{4} H [X_{2}], \\ d [X_{1}^{0}; X_{1} | X_{1} + {\tilde{X}}_{2}] - d [X_{1}^{0}; X_{1}] & \leq \frac{1}{2} k + \frac{1}{4} H [X_{1}] - \frac{1}{4} H [X_{2}] \\ d [X_{2}^{0}; X_{2} | X_{2} + {\tilde{X}}_{1}] - d [X_{2}^{0}; X_{2}] & \leq \frac{1}{2} k + \frac{1}{4} H [X_{2}] - \frac{1}{4} H [X_{1}] . \end{aligned}

LaTeX

Lean

diff_rdist_le_1
diff_rdist_le_2
diff_rdist_le_3
diff_rdist_le_4

Lemma 3.25Comparison of Ruzsa distances, I

Let $X, Y, Z$ be random variables taking values in some abelian group of characteristic $2$ , and with $Y, Z$ independent. Then we have

\begin{aligned} d [X; Y + Z] - d [X; Y] & \leq \frac{1}{2} (H [Y + Z] - H [Y]) \\ = \frac{1}{2} d [Y; Z] + \frac{1}{4} H [Z] - \frac{1}{4} H [Y] . \end{aligned}

and

\begin{aligned} d [X; Y | Y + Z] - d [X; Y] & \leq \frac{1}{2} (H [Y + Z] - H [Z]) \\ = \frac{1}{2} d [Y; Z] + \frac{1}{4} H [Y] - \frac{1}{4} H [Z] . \end{aligned}

LaTeX

Lean

condRuzsaDist_diff_le
condRuzsaDist_diff_le'
condRuzsaDist_diff_le''
condRuzsaDist_diff_le'''

Lemma 6.13Entropy bound on quadruple sum

With the same notation, we have

H [X_{1} + X_{2} + {\tilde{X}}_{1} + {\tilde{X}}_{2}] \leq \frac{1}{2} H [X_{1}] + \frac{1}{2} H [X_{2}] + (2 + η) k - I_{1} .

LaTeX Lean

Lemma 8.5General inequality

Let $X_{1}, X_{2}, X_{3}, X_{4}$ be independent $G$ -valued random variables, and let $Y$ be another $G$ -valued random variable. Set $S := X_{1} + X_{2} + X_{3} + X_{4}$ . Then

\begin{aligned} d [Y; X_{1} + X_{2} | X_{1} + X_{3}, S] - d [Y; X_{1}] \\ \leq \frac{1}{4} (d [X_{1}; X_{2}] + 2 d [X_{1}; X_{3}] + d [X_{2}; X_{4}]) \\ + \frac{1}{4} (d [X_{1} | X_{1} + X_{3}; X_{2} | X_{2} + X_{4}] - d [X_{3} | X_{3} + X_{4}; X_{1} | X_{1} + X_{2}]) \\ + \frac{1}{8} (H [X_{1} + X_{2}] - H [X_{3} + X_{4}] + H [X_{2}] - H [X_{3}] \\ + H [X_{2} | X_{2} + X_{4}] - H [X_{1} | X_{1} + X_{3}]) . \end{aligned}

LaTeX Lean

Lemma 13.3Gibbs inequality

$D_{K L} (X ‖ Y) \geq 0$ .

LaTeX Lean

Lemma 13.4Converse Gibbs inequality

If $D_{K L} (X ‖ Y) = 0$ , then $Y$ is a copy of $X$ .

LaTeX Lean

Lemma 9.2Goursat type theorem

Let $H$ be a subgroup of $G \times G^{'}$ . Then there exists a subgroup $H_{0}$ of $G$ , a subgroup $H_{1}$ of $G^{'}$ , and a homomorphism $ϕ : G \to G^{'}$ such that

H := {(x, ϕ (x) + y) : x \in H_{0}, y \in H_{1}} .

In particular, $| H | = | H_{0} | | H_{1} |$ .

LaTeX Lean

Lemma 9.1Hahn-Banach type theorem

Let $H_{0}$ be a subgroup of $G$ . Then every homomorphism $ϕ : H_{0} \to G^{'}$ can be extended to a homomorphism $\tilde{ϕ} : G \to G^{'}$ .

LaTeX Lean

Theorem 9.3Homomorphism form of PFR

Let $f : G \to G^{'}$ be a function, and let $S$ denote the set

S := {f (x + y) - f (x) - f (y) : x, y \in G} .

Then there exists a homomorphism $ϕ : G \to G^{'}$ such that

| {f (x) - ϕ (x) : x \in G} | \leq | S |^{10} .

LaTeX Lean

Lemma 13.31

$d [X_{1}; X_{1}] + d [X_{2}; X_{2}] = 2 d [X_{1}; X_{2}] + (I_{2} - I_{1})$ .

LaTeX Lean

Definition 2.22Independent random variables

Two random variables $X : Ω \to S$ and $Y : Ω \to T$ are independent if the law of $(X, Y)$ is the product of the law of $X$ and the law of $Y$ . Similarly for more than two variables.

LaTeX Lean

Lemma 3.7Existence of independent copies

Let $X_{i} : Ω_{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}$ .

LaTeX

Lean

ProbabilityTheory.independent_copies
ProbabilityTheory.independent_copies'
ProbabilityTheory.independent_copies_two
ProbabilityTheory.independent_copies3_nondep

Definition 2.15Mutual information

If $X : Ω \to S$ , $Y : Ω \to T$ are random variables, then

I [X : Y] := H [X] + H [Y] - H [X, Y] .

LaTeX

Lean

ProbabilityTheory.mutualInfo
ProbabilityTheory.mutualInfo_def

Lemma 1.2Jensen

If $S$ is a finite set, and $\sum_{s \in S} w_{s} = 1$ for some non-negative $w_{s}$ , and $p_{s} \in [0, 1]$ for all $s \in S$ , then

\sum_{s \in S} w_{s} h (p_{s}) \leq h (\sum_{s \in S} w_{s} p_{s}) .

LaTeX Lean

Lemma 2.3Jensen bound

If $X$ is an $S$ -valued random variable, then $H [X] \leq \log | S |$ .

LaTeX

Lean

ProbabilityTheory.entropy_le_log_card
ProbabilityTheory.entropy_le_log_card_of_mem

Proposition 12.46Vanishing entropy

We have $k = 0$ .

LaTeX

Proposition 12.37Bounding mutual information

Suppose that $X_{i, j}$ , $1 \leq i, j \leq m$ , are jointly independent $G$ -valued random variables, such that for each $j = 1, \dots, m$ , the random variables $(X_{i, j})_{i = 1}^{m}$ coincide in distribution with some permutation of $X_{[m]}$ . Write

I := I [(\sum_{i = 1}^{m} X_{i, j})_{j = 1}^{m} : (\sum_{j = 1}^{m} X_{i, j})_{i = 1}^{m} | \sum_{i = 1}^{m} \sum_{j = 1}^{m} X_{i, j}] .

Then

I \leq 4 m^{2} η k .

LaTeX Lean

Lemma 6.20Key identity

We have $U + V + W = 0$ .

LaTeX Lean

Lemma 13.9Kullback–Leibler and conditioning

If $X, Y$ are independent $G$ -valued random variables, and $Z$ is another random variable defined on the same sample space as $X$ , then

D_{K L} ((X | Z) ‖ Y) = D_{K L} (X ‖ Y) + H [X] - H [X | Z] .

LaTeX Lean

Definition 13.1Kullback–Leibler divergence

If $X, Y$ are two $G$ -valued random variables, the Kullback–Leibler divergence is defined as

D_{K L} (X ‖ Y) := \sum_{x} P (X = x) \log \frac{P (X = x)}{P (Y = x)} .

LaTeX Lean

Lemma 13.5Convexity of Kullback–Leibler

If $S$ is a finite set, $\sum_{s \in S} w_{s} = 1$ for some non-negative $w_{s}$ , and $P (X = x) = \sum_{s \in S} w_{s} P (X_{s} = x)$ , $P (Y = x) = \sum_{s \in S} w_{s} P (Y_{s} = x)$ for all $x$ , then

D_{K L} (X ‖ Y) \leq \sum_{s \in S} w_{s} D_{K L} (X_{s} ‖ Y_{s}) .

LaTeX Lean

Lemma 13.2Kullback–Leibler divergence of copy

If $X^{'}$ is a copy of $X$ , and $Y^{'}$ is a copy of $Y$ , then $D_{K L} (X^{'} ‖ Y^{'}) = D_{K L} (X ‖ Y)$ .

LaTeX Lean

Lemma 13.6Kullback–Leibler and injections

If $f : G \to H$ is an injection, then $D_{K L} (f (X) ‖ f (Y)) = D_{K L} (X ‖ Y)$ .

LaTeX Lean

Lemma 13.7Kullback–Leibler and sums

If $X, Y, Z$ are independent $G$ -valued random variables, then

D_{K L} (X + Z ‖ Y + Z) \leq D_{K L} (X ‖ Y) .

LaTeX Lean

Lemma 12.6Kaimonovich–Vershik–Madiman inequality

If $n \geq 0$ and $X, Y_{1}, \dots, Y_{n}$ are jointly independent $G$ -valued random variables, then

H [X + \sum_{i = 1}^{n} Y_{i}] - H [X] \leq \sum_{i = 1}^{n} (H [X + Y_{i}] - H [X]) .

LaTeX Lean

Lemma 12.7Kaimonovich–Vershik–Madiman inequality, II

If $n \geq 1$ and $X, Y_{1}, \dots, Y_{n}$ are jointly independent $G$ -valued random variables, then

d [X; \sum_{i = 1}^{n} Y_{i}] \leq 2 \sum_{i = 1}^{n} d [X; Y_{i}] .

LaTeX Lean

Lemma 12.8Kaimonovich–Vershik–Madiman inequality, III

If $n \geq 1$ and $X, Y_{1}, \dots, Y_{n}$ are jointly independent $G$ -valued random variables, then

d [X; \sum_{i = 1}^{n} Y_{i}] \leq d [X; Y_{1}] + \frac{1}{2} (H [\sum_{i = 1}^{n} Y_{i}] - H [Y_{1}]) .

LaTeX Lean

Lemma 3.21Kaimanovich-Vershik-Madiman inequality

Suppose that $X, Y, Z$ are independent $G$ -valued random variables. Then

H [X + Y + Z] - H [X + Y] \leq H [Y + Z] - H [Y] .

LaTeX Lean

Corollary 4.6General 100% inverse theorem

Suppose that $X_{1}, X_{2}$ are $G$ -valued random variables such that $d [X_{1}; X_{2}] = 0$ . Then there exists a subgroup $H \leq G$ such that $d [X_{1}; U_{H}] = d [X_{2}; U_{H}] = 0$ .

LaTeX Lean

Lemma 4.5Symmetric 100% inverse theorem

Suppose that $X$ is a $G$ -valued random variable such that $d [X; X] = 0$ . Then there exists a subgroup $H \leq G$ such that $d [X; U_{H}] = 0$ .

LaTeX Lean

Lemma 12.45Application of BSG

Let $G$ be an abelian group, let $(T_{1}, T_{2}, T_{3})$ be a $G^{3}$ -valued random variable such that $T_{1} + T_{2} + T_{3} = 0$ holds identically, and write

δ := I [T_{1} : T_{2}] + I [T_{1} : T_{3}] + I [T_{2} : T_{3}] .

Let $Y_{1}, \dots, Y_{n}$ be some further $G$ -valued random variables and let $α > 0$ be a constant. Then there exists a random variable $U$ such that

d [U; U] + α \sum_{i = 1}^{n} d [Y_{i}; U] \leq (2 + \frac{α n}{2}) δ + α \sum_{i = 1}^{n} d [Y_{i}; T_{2}] .

LaTeX Lean

Lemma 1.4log sum inequality

If $S$ is a finite set, and $a_{s}, b_{s}$ are non-negative for $s \in S$ , then

\sum_{s \in S} a_{s} \log \frac{a_{s}}{b_{s}} \geq (\sum_{s \in S} a_{s}) \log \frac{\sum_{s \in S} a_{s}}{\sum_{s \in S} b_{s}},

with the convention $0 \log \frac{0}{b} = 0$ for any $b \geq 0$ and $0 \log \frac{a}{0} = \infty$ for any $a > 0$ .

LaTeX Lean

Theorem 12.47Entropy form of PFR

Suppose that $G$ is a finite abelian group of torsion $m$ . Suppose that $X$ is a $G$ -valued random variable. Then there exists a subgroup $H \leq G$ such that

d [X; U_{H}] \leq 64 m^{3} d [X; X] .

LaTeX Lean

Definition 12.38Additional random variables

By a slight abuse of notation, we identify $Z / m Z$ and ${1, \dots, m}$ in the obvious way, and let $Y_{i, j}$ be an independent copy of $X_{i}$ for $i, j \in Z / m Z$ . Then also define:

W := \sum_{i, j \in Z / m Z} Y_{i, j}

and

Z_{1} := \sum_{i, j \in Z / m Z} i Y_{i, j}, Z_{2} := \sum_{i, j \in Z / m Z} j Y_{i, j}, Z_{3} := \sum_{i, j \in Z / m Z} (- i - j) Y_{i, j} .

The addition $(- i - j)$ takes place over $Z / m Z$ . Note that, because we are assuming $G$ is $m$ -torsion, it is well-defined to multiply elements of $G$ by elements of $Z / m Z$ . We will also define for $i, j, r \in Z / m Z$ the variables

P_{i} := \sum_{j \in Z / m Z} Y_{i, j}, Q_{j} := \sum_{i \in Z / m Z} Y_{i, j}, R_{r} := \sum_{\begin{matrix} i, j \in Z / m Z \\ i + j = - r \end{matrix}} Y_{i, j} .

LaTeX

Proposition 12.21Vanishing

If $D [X_{[m]}] = 0$ , then for each $1 \leq i \leq m$ there is a finite subgroup $H_{i} \leq G$ such that $d [X_{i}; U_{H_{i}}] = 0$ .

LaTeX Lean

Lemma 12.33Multidistance chain rule

Let $π : G \to H$ be a homomorphism of abelian groups and let $X_{[m]}$ be a tuple of jointly independent $G$ -valued random variables. Then $D [X_{[m]}]$ is equal to

D [X_{[m]} | π (X_{[m]})] + D [π (X_{[m]})] + I [\sum_{i = 1}^{m} X_{i} : π (X_{[m]}) | π (\sum_{i = 1}^{m} X_{i})]

where $π (X_{[m]}) := (π (X_{i}))_{1 \leq i \leq m}$ .

LaTeX Lean

Lemma 12.34Conditional multidistance chain rule

Let $π : G \to H$ be a homomorphism of abelian groups. Let $I$ be a finite index set and let $X_{[m]}$ be a tuple of $G$ -valued random variables. Let $Y_{[m]}$ be another tuple of random variables (not necessarily $G$ -valued). Suppose that the pairs $(X_{i}, Y_{i})$ are jointly independent of one another (but $X_{i}$ need not be independent of $Y_{i}$ ). Then

\begin{aligned} D [X_{[m]} | Y_{[m]}] & = D [X_{[m]} | π (X_{[m]}), Y_{[m]}] + D [π (X_{[m]}) | Y_{[m]}] \\ + I [\sum_{i = 1}^{m} X_{i} : π (X_{[m]}) | π (\sum_{i = 1}^{m} X_{i}), Y_{[m]}] . \end{aligned}

LaTeX Lean

Lemma 12.35

Let $m$ be a positive integer. Suppose one has a sequence

G_{m} \to G_{m - 1} \to \dots \to G_{1} \to G_{0} = {0}

of homomorphisms between abelian groups $G_{0}, \dots, G_{m}$ , and for each $d = 0, \dots, m$ , let $π_{d} : G_{m} \to G_{d}$ be the homomorphism from $G_{m}$ to $G_{d}$ arising from this sequence by composition (so for instance $π_{m}$ is the identity homomorphism and $π_{0}$ is the zero homomorphism). Let $X_{[m]} = (X_{i})_{1 \leq i \leq m}$ be a jointly independent tuple of $G_{m}$ -valued random variables. Then

\begin{aligned} D [X_{[m]}] & = \sum_{d = 1}^{m} D [π_{d} (X_{[m]}) | π_{d - 1} (X_{[m]})] \\ + \sum_{d = 1}^{m - 1} I [\sum_{i} X_{i} : π_{d} (X_{[m]}) | π_{d} (\sum_{i} X_{i}), π_{d - 1} (X_{[m]})] . \end{aligned}

In particular, by Lemma 2.27,

\begin{aligned} D [X_{[m]}] \geq & \sum_{d = 1}^{m} D [π_{d} (X_{[m]}) | π_{d - 1} (X_{[m]})] \\ + I [\sum_{i} X_{i} : π_{1} (X_{[m]}) | π_{1} (\sum_{i} X_{i})] . \end{aligned}

LaTeX

Lean

iter_multiDist_chainRule
iter_multiDist_chainRule'

Lemma 12.13Multidistance of copy

If $X_{[m]} = (X_{i})_{1 \leq i \leq m}$ and $Y_{[m]} = (Y_{i})_{1 \leq i \leq m}$ are such that $X_{i}$ and $Y_{i}$ have the same distribution for each $i$ , then $D [X_{[m]}] = D [Y_{[m]}]$ .

LaTeX Lean

Definition 12.12Multidistance

Let $m$ be a positive integer, and let $X_{[m]} = (X_{i})_{1 \leq i \leq m}$ be an $m$ -tuple of $G$ -valued random variables $X_{i}$ . Then we define

D [X_{[m]}] := H [\sum_{i = 1}^{m} {\tilde{X}}_{i}] - \frac{1}{m} \sum_{i = 1}^{m} H [{\tilde{X}}_{i}],

where the ${\tilde{X}}_{i}$ are independent copies of the $X_{i}$ .

LaTeX Lean

Lemma 12.14Multidistance of independent variables

If $X_{[m]} = (X_{i})_{1 \leq i \leq m}$ are jointly independent, then $D [X_{[m]}] = H [\sum_{i = 1}^{m} X_{i}] - \frac{1}{m} \sum_{i = 1}^{m} H [X_{i}]$ .

LaTeX Lean

Lemma 12.27Lower bound on multidistance

If $(X_{i})_{1 \leq i \leq m}$ is a $τ$ -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 η \sum_{i = 1}^{m} d [X_{i}; X_{i}^{'}] .

LaTeX Lean

Lemma 12.15Nonnegativity

For any such tuple, we have $D [X_{[m]}] \geq 0$ .

LaTeX Lean

Lemma 12.16Relabeling

If $ϕ : {1, \dots, m} \to {1, \dots, m}$ is a bijection, then $D [X_{[m]}] = D [(X_{ϕ (j)})_{1 \leq j \leq m}]$ .

LaTeX Lean

Lemma 12.17Multidistance and Ruzsa distance, I

Let $m \geq 2$ , and let $X_{[m]}$ be a tuple of $G$ -valued random variables. Then

\sum_{1 \leq j, k \leq m : j \neq k} d [X_{j}; - X_{k}] \leq m (m - 1) D [X_{[m]}] .

LaTeX Lean

Lemma 12.18Multidistance and Ruzsa distance, II

Let $m \geq 2$ , and let $X_{[m]}$ be a tuple of $G$ -valued random variables. Then

\sum_{j = 1}^{m} d [X_{j}; X_{j}] \leq 2 m D [X_{[m]}] .

LaTeX Lean

Lemma 12.19Multidistance and Ruzsa distance, III

Let $m \geq 2$ , and let $X_{[m]}$ be a tuple of $G$ -valued random variables. If the $X_{i}$ all have the same distribution, then $D [X_{[m]}] \leq m d [X_{i}; X_{i}]$ for any $1 \leq i \leq m$ .

LaTeX Lean

Lemma 12.20Multidistance and Ruzsa distance, IV

Let $m \geq 2$ , and let $X_{[m]}$ be a tuple of independent $G$ -valued random variables. Let $W := \sum_{i = 1}^{m} X_{i}$ . Then

d [W; - W] \leq 2 D [X_{i}] .

LaTeX Lean

Lemma 2.17Nonnegativity of mutual information

We have $I [X : Y] \geq 0$ .

LaTeX Lean

Lemma 12.43Mutual information bound

We have $I [W : Z_{2}] \leq 2 (m - 1) k$ .

LaTeX Lean

Lemma 3.1Negation preserves entropy

If $X$ is $G$ -valued, then $H [- X] = H [X]$ .

LaTeX Lean

Theorem 7.3PFR

If $A \subset F_{2}^{n}$ is non-empty and $| A + A | \leq K | A |$ , then $A$ can be covered by most $2 K^{12}$ translates of a subspace $H$ of $F_{2}^{n}$ with $| H | \leq | A |$ .

LaTeX Lean

Theorem 13.41PFR with

C = 9

If $A \subset F_{2}^{n}$ is finite non-empty with $| A + A | \leq K | A |$ , then there exists a subgroup $H$ of $F_{2}^{n}$ with $| H | \leq | A |$ such that $A$ can be covered by at most $2 K^{9}$ translates of $H$ .

LaTeX Lean

Corollary 13.39

If $| A + A | \leq K | A |$ , then there exists a subgroup $H$ and $t \in G$ such that $| A \cap (H + t) | \geq K^{- 4} \sqrt{| A | | H |}$ , and $| H | / | A | \in [K^{- 8}, K^{8}]$ .

LaTeX Lean

Corollary 13.40

If $| A + A | \leq K | A |$ , then there exist a subgroup $H$ and a subset $c$ of $G$ with $A \subseteq c + H$ , such that $| c | \leq K^{5} | A |^{1 / 2} / | H |^{1 / 2}$ and $| H | / | A | \in [K^{- 8}, K^{8}]$ .

LaTeX Lean

Corollary 7.4PFR in infinite groups

If $G$ is an abelian $2$ -torsion group, $A \subset G$ is non-empty finite, and $| A + A | \leq K | A |$ , then $A$ can be covered by most $2 K^{12}$ translates of a finite group $H$ of $G$ with $| H | \leq | A |$ .

LaTeX Lean

Theorem 8.11Improved PFR

If $A \subset F_{2}^{n}$ is non-empty and $| A + A | \leq K | A |$ , then $A$ can be covered by most $2 K^{11}$ translates of a subspace $H$ of $F_{2}^{n}$ with $| H | \leq | A |$ .

LaTeX Lean

Lemma 11.5

If $G = F_{2}^{d}$ and $α \in (0, 1)$ and $X, Y$ are $G$ -valued random variables then there is a subgroup $H \leq F_{2}^{d}$ such that

\log | H | \leq 2 (H (X) + H (Y))

and if $ψ : G \to G / H$ is the natural projection then

H (ψ (X)) + H (ψ (Y)) \leq 34 d [ψ (X); ψ (Y)] .

LaTeX Lean

Lemma 11.4

If $G = F_{2}^{d}$ and $α \in (0, 1)$ and $X, Y$ are $G$ -valued random variables then there is a subgroup $H \leq F_{2}^{d}$ such that

\log | H | \leq \frac{1 + α}{2 (1 - α)} (H (X) + H (Y))

and if $ψ : G \to G / H$ is the natural projection then

H (ψ (X)) + H (ψ (Y)) \leq \frac{20}{α} d [ψ (X); ψ (Y)] .

LaTeX Lean

Proposition 13.38

For any random variables $Y_{1}, Y_{2}$ , there exist a subgroup $H$ such that

2 ρ (U_{H}) \leq ρ (Y_{1}) + ρ (Y_{2}) + 8 d [Y_{1}; Y_{2}] .

LaTeX Lean

Theorem 12.49PFR

Suppose that $G$ is a finite abelian group of torsion $m$ . If $A \subset G$ is non-empty and $| A + A | \leq K | A |$ , then $A$ can be covered by most $m K^{96 m^{3} + 2}$ translates of a subspace $H$ of $G$ with $| H | \leq | A |$ .

LaTeX Lean

Lemma 7.2

If $A \subset F_{2}^{n}$ is non-empty and $| A + A | \leq K | A |$ , then $A$ can be covered by at most $K^{13 / 2} | A |^{1 / 2} / | H |^{1 / 2}$ translates of a subspace $H$ of $F_{2}^{n}$ with

| H | / | A | \in [K^{- 11}, K^{11}] .

LaTeX Lean

Lemma 8.10

If $A \subset F_{2}^{n}$ is non-empty and $| A + A | \leq K | A |$ , then $A$ can be covered by at most $K^{6} | A |^{1 / 2} / | H |^{1 / 2}$ translates of a subspace $H$ of $F_{2}^{n}$ with

| H | / | A | \in [K^{- 10}, K^{10}] .

LaTeX Lean

Lemma 12.48

Suppose that $G$ is a finite abelian group of torsion $m$ . If $A \subset G$ is non-empty and $| A + A | \leq K | A |$ , then $A$ can be covered by at most $K^{(64 m^{3} + 2) / 2} | A |^{1 / 2} / | H |^{1 / 2}$ translates of a subspace $H$ of $G$ with

| H | / | A | \in [K^{- 64 m^{3}}, K^{64 m^{3}}] .

LaTeX Lean

Lemma 13.30

$I_{1} \leq 2 η d [X_{1}; X_{2}]$

LaTeX Lean

Definition 13.28

Given $G$ -valued random variables $X, Y$ , define

ϕ [X; Y] := d [X; Y] + η (ρ (X) + ρ (Y))

and define a $ϕ$ -minimizer to be a pair of random variables $X, Y$ which minimizes $ϕ [X; Y]$ .

LaTeX Lean

Lemma 13.29

ϕ

-minimizers exist

There exists a $ϕ$ -minimizer.

LaTeX Lean

Proposition 13.37

If $X_{1}, X_{2}$ is a $ϕ$ -minimizer, then $d [X_{1}; X_{2}] = 0$ .

LaTeX Lean

Lemma 13.32

$I_{2} \leq 2 η d [X_{1}; X_{2}] + \frac{η}{1 - η} (2 η d [X_{1}; X_{2}] - I_{1})$ .

LaTeX Lean

Proposition 12.40Mutual information bound

We have

I [Z_{1} : Z_{2} | W], I [Z_{2} : Z_{3} | W], I [Z_{1} : Z_{3} | W] \leq t

where

t := 4 m^{2} η k .

LaTeX

Lean

mutual_information_le_t_12
mutual_information_le_t_13
mutual_information_le_t_23

Lemma 2.2Entropy and relabeling

If $X : Ω \to S$ and $Y : Ω \to T$ are random variables, and $Y = f (X)$ for some injection $f : S \to T$ , then $H [X] = H [Y]$ .
If $X : Ω \to S$ and $Y : Ω \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 $H [X] = H [Y]$ .

LaTeX

Lean

ProbabilityTheory.entropy_comp_of_injective
ProbabilityTheory.entropy_of_comp_eq_of_comp

Lemma 2.12Conditional entropy and relabeling

If $X : Ω \to S$ , $Y : Ω \to T$ , and $Z : Ω \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 $H [X | Z] = H [Y | Z]$ .

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

LaTeX

Lean

ProbabilityTheory.condEntropy_comp_of_injective
ProbabilityTheory.condEntropy_of_injective'

Lemma 13.33

If $G$ -valued random variables $T_{1}, T_{2}, T_{3}$ satisfy $T_{1} + T_{2} + T_{3} = 0$ , then

d [X_{1}; X_{2}] \leq 3 I [T_{1} : T_{2}] + (2 H [T_{3}] - H [T_{1}] - H [T_{2}]) + η (ρ (T_{1} | T_{3}) + ρ (T_{2} | T_{3}) - ρ (X_{1}) - ρ (X_{2})) .

LaTeX Lean

Lemma 13.34

If $G$ -valued random variables $T_{1}, T_{2}, T_{3}$ satisfy $T_{1} + T_{2} + T_{3} = 0$ , then

d [X_{1}; X_{2}] \leq \sum_{1 \leq i < j \leq 3} I [T_{i} : T_{j}] + \frac{η}{3} \sum_{1 \leq i < j \leq 3} (ρ (T_{i} | T_{j}) + ρ (T_{j} | T_{i}) - ρ (X_{1}) - ρ (X_{2}))

LaTeX Lean

Lemma 13.25Rho and conditioning

If $X, Z$ are defined on the same space, one has

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

ρ^{+} (X | Z) \leq ρ^{+} (X)

and

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

LaTeX

Lean

condRhoMinus_le
condRhoPlus_le
condRho_le

Definition 13.22Conditional Rho functional

We define $ρ (X | Y) := \sum_{y} P (Y = y) ρ (X | Y = y)$ .

LaTeX Lean

Lemma 13.23Conditional rho and translation

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

LaTeX Lean

Lemma 13.24Conditional rho and relabeling

If $f$ is injective, then $ρ (X | f (Y)) = ρ (X | Y)$ .

LaTeX Lean

Lemma 13.27Rho and conditioning, symmetrized

If $X, Y$ are independent, then

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

LaTeX Lean

Lemma 13.20Rho continuous

$ρ (X)$ depends continuously on the distribution of $X$ .

LaTeX Lean

Definition 13.16Rho functional

We define $ρ (X) := (ρ^{+} (X) + ρ^{-} (X)) / 2$ .

LaTeX Lean

Lemma 13.35

For independent random variables $Y_{1}, Y_{2}, Y_{3}, Y_{4}$ over $G$ , define $S := Y_{1} + Y_{2} + Y_{3} + Y_{4}$ , $T_{1} := Y_{1} + Y_{2}$ , $T_{2} := Y_{1} + Y_{3}$ . Then

ρ (T_{1} | T_{2}, S) + ρ (T_{2} | T_{1}, S) - \frac{1}{2} \sum_{i} ρ (Y_{i}) \leq \frac{1}{2} (d [Y_{1}; Y_{2}] + d [Y_{3}; Y_{4}] + d [Y_{1}; Y_{3}] + d [Y_{2}; Y_{4}]) .

LaTeX Lean

Lemma 13.36

For independent random variables $Y_{1}, Y_{2}, Y_{3}, Y_{4}$ over $G$ , define $T_{1} := Y_{1} + Y_{2}, T_{2} := Y_{1} + Y_{3}, T_{3} := Y_{2} + Y_{3}$ and $S := Y_{1} + Y_{2} + Y_{3} + Y_{4}$ . Then

\sum_{1 \leq i < j \leq 3} (ρ (T_{i} | T_{j}, S) + ρ (T_{j} | T_{i}, S) - \frac{1}{2} \sum_{i} ρ (Y_{i})) \leq \sum_{1 \leq i < j \leq 4} d [Y_{i}; Y_{j}]

LaTeX Lean

Lemma 13.19Rho invariant

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

LaTeX Lean

Lemma 13.18Rho of subgroup

If $H$ is a finite subgroup of $G$ , and $ρ (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^{- 2 r}, e^{2 r}]$ .

LaTeX Lean

Lemma 13.21Rho and sums

If $X, Y$ are independent, one has

ρ^{-} (X + Y) \leq ρ^{-} (X)

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

and

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

LaTeX

Lean

rhoMinus_of_sum
rhoPlus_of_sum
rho_of_sum

Lemma 13.26Rho and sums, symmetrized

If $X, Y$ are independent, then

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

LaTeX Lean

Lemma 13.17

We have $ρ (U_{A}) = 0$ .

LaTeX

Definition 13.11Rho minus

For any $G$ -valued random variable $X$ , we define $ρ^{-} (X)$ to be the infimum of $D_{K L} (X ‖ U_{A} + T)$ , where $U_{A}$ is uniform on $A$ and $T$ ranges over $G$ -valued random variables independent of $U_{A}$ .

LaTeX Lean

Lemma 13.14Rho minus of subgroup

If $H$ is a finite subgroup of $G$ , then $ρ^{-} (U_{H}) = \log | A | - \log max_{t} | A \cap (H + t) |$ .

LaTeX Lean

Lemma 13.13Rho minus non-negative

We have $ρ^{-} (X) \geq 0$ .

LaTeX

Definition 13.12Rho plus

For any $G$ -valued random variable $X$ , we define $ρ^{+} (X) := ρ^{-} (X) + H (X) - H (U_{A})$ .

LaTeX Lean

Corollary 13.15Rho plus of subgroup

If $H$ is a finite subgroup of $G$ , then $ρ^{+} (U_{H}) = \log | H | - \log max_{t} | A \cap (H + t) |$ .

LaTeX Lean

Lemma 3.10Copy preserves Ruzsa distance

If $X^{'}, Y^{'}$ are copies of $X, Y$ respectively then $d [X^{'}; Y^{'}] = d [X; Y]$ .

LaTeX Lean

Lemma 7.1Ruzsa covering lemma

If $A, B$ are finite non-empty subsets of a group $G$ , then $A$ can be covered by at most $| A + B | / | B |$ translates of $B - B$ .

LaTeX Lean

Definition 3.8Ruzsa 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] := H [X^{'} - Y^{'}] - H [X^{'}] / 2 - H [Y^{'}] / 2

where $X^{'}, Y^{'}$ are (the canonical) independent copies of $X, Y$ from Lemma 3.7.

LaTeX Lean

Lemma 3.11Ruzsa distance in independent case

If $X, Y$ are independent $G$ -random variables then

d [X; Y] := H [X - Y] - H [X] / 2 - H [Y] / 2.

LaTeX Lean

Lemma 3.13Distance controls entropy difference

If $X, Y$ are $G$ -valued random variables, then

| H [X] - H [Y] | \leq 2 d [X; Y] .

LaTeX Lean

Lemma 3.14Distance controls entropy growth

If $X, Y$ are independent $G$ -valued random variables, then

H [X - Y] - H [X], H [X - Y] - H [Y] \leq 2 d [X; Y] .

LaTeX

Lean

diff_ent_le_rdist'
diff_ent_le_rdist''

Lemma 3.15Distance nonnegative

If $X, Y$ are $G$ -valued random variables, then

d [X; Y] \geq 0.

LaTeX Lean

Lemma 3.12Distance symmetric

If $X, Y$ are $G$ -valued random variables, then

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

LaTeX Lean

Lemma 3.18Ruzsa triangle inequality

If $X, Y, Z$ are $G$ -valued random variables, then

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

LaTeX Lean

Lemma 3.17Improved Ruzsa triangle inequality

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

H [X - Y] \leq H [X - Z] + H [Z - Y] - H [Z]

LaTeX Lean

Lemma 6.16Second estimate

We have

I_{2} \leq 2 η k + \frac{2 η (2 η k - I_{1})}{1 - η} .

LaTeX Lean

Lemma 6.15

We have

d [X_{1}; X_{1}] + d [X_{2}; X_{2}] \leq 2 k + \frac{2 (2 η k - I_{1})}{1 - η} .

LaTeX Lean

Lemma 3.26Comparison of Ruzsa distances, II

Let $X, Y, Z, Z^{'}$ be random variables taking values in some abelian group, and with $Y, Z, Z^{'}$ independent. Then we have

\begin{aligned} d [X; Y + Z | Y + Z + Z^{'}] - d [X; Y] \\ \leq \frac{1}{2} (H [Y + Z + Z^{'}] + H [Y + Z] - H [Y] - H [Z^{'}]) . \end{aligned}

LaTeX Lean

Lemma 3.2Shearing preserves entropy

If $X, Y$ are $G$ -valued, then $H [X \pm Y | Y] = H [X | Y]$ and $H [X \pm Y, Y] = H [X, Y]$ .

LaTeX

Lean

ProbabilityTheory.condEntropy_add_right
ProbabilityTheory.condEntropy_add_left
ProbabilityTheory.condEntropy_sub_right
ProbabilityTheory.condEntropy_sub_left

Lemma 12.5Flipping a sign

If $X, Y$ are $G$ -valued, then

d [X; - Y] \leq 3 d [X; Y] .

LaTeX Lean

Lemma 11.6

Let $ϕ : G \to H$ be a homomorphism and $A, B \subseteq G$ be finite subsets. If $x, y \in H$ then let $A_{x} = A \cap ϕ^{- 1} (x)$ and $B_{y} = B \cap ϕ^{- 1} (y)$ . There exist $x, y \in H$ such that $A_{x}, B_{y}$ are both non-empty and

d [ϕ (U_{A}); ϕ (U_{B})] \log \frac{| A | | B |}{| A_{x} | | B_{y} |} \leq (H (ϕ (U_{A})) + H (ϕ (U_{B}))) (d (U_{A}, U_{B}) - d (U_{A_{x}}, U_{B_{y}})) .

LaTeX Lean

Corollary 2.18Subadditivity

With notation as above, we have $H [X, Y] \leq H [X] + H [Y]$ .

LaTeX Lean

Corollary 2.20Submodularity

With three random variables $X, Y, Z$ , one has $H [X | Y, Z] \leq H [X | Z]$ .

LaTeX

Lean

ProbabilityTheory.entropy_submodular
ProbabilityTheory.condEntropy_comp_ge

Lemma 12.10Sums of dilates I

Let $X, Y, X^{'}$ be independent $G$ -valued random variables, with $X^{'}$ a copy of $X$ , and let $a$ be an integer. Then

H [X - (a + 1) Y] \leq H [X - a Y] + H [X - Y - X^{'}] - H [X]

and

H [X - (a - 1) Y] \leq H [X - a Y] + H [X - Y - X^{'}] - H [X] .

LaTeX

Lean

ent_of_sub_smul
ent_of_sub_smul'

Lemma 12.11Sums of dilates II

Let $X, Y$ be independent $G$ -valued random variables, and let $a$ be an integer. Then

H [X - a Y] - H [X] \leq 4 | a | d [X; Y] .

LaTeX Lean

Corollary 3.5Independent lower bound on sumset

If $X, Y$ are independent $G$ -valued random variables, then

max (H [X], H [Y]) \leq H [X \pm Y] .

LaTeX

Lean

max_entropy_le_entropy_add
max_entropy_le_entropy_sub

Lemma 3.3Lower bound of sumset

If $X, Y$ are $G$ -valued random variables on $Ω$ , we have

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

LaTeX

Lean

ProbabilityTheory.max_entropy_sub_mutualInfo_le_entropy_add
ProbabilityTheory.max_entropy_sub_mutualInfo_le_entropy_sub

Corollary 3.4Conditional lower bound on sumset

If $X, Y$ are $G$ -valued random variables on $Ω$ and $Z$ is another random variable on $Ω$ then

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

LaTeX

Lean

ProbabilityTheory.max_condEntropy_sub_condMutualInfo_le_condEntropy_mul
ProbabilityTheory.max_condEntropy_sub_condMutualInfo_le_condEntropy_div

Lemma 4.2Symmetry group is a group

If $X$ is a $G$ -valued random variable, then $Sym [X]$ is a subgroup of $G$ .

LaTeX Lean

Definition 4.1Symmetry group

If $X$ is a $G$ -valued random variable, then the symmetry group $Sym [X]$ is the set of all $h \in G$ such that $X + h$ has the same distribution as $X$ .

LaTeX Lean

Lemma 4.4Translate is uniform on symmetry group

If $X$ is a $G$ -valued random variable with $d [X; X] = 0$ , and $x_{0}$ is a point with $P [X = x_{0}] > 0$ , then $X - x_{0}$ is uniformly distributed on $Sym [X]$ .

LaTeX Lean

Lemma 6.17Symmetry identity

We have

I (U : W | S) = I (V : W | S) .

LaTeX Lean

Lemma 6.3

τ

depends only on distribution

If $X_{1}^{'}, X_{2}^{'}$ are copies of $X_{1}, X_{2}$ , then $τ [X_{1}^{'}; X_{2}^{'}] = τ [X_{1}; X_{2}]$ .

LaTeX Lean

Definition 6.2

τ

functional

If $X_{1}, X_{2}$ are two $G$ -valued random variables, then

τ [X_{1}; X_{2}] := d [X_{1}; X_{2}] + η d [X_{1}^{0}; X_{1}] + η d [X_{2}^{0}; X_{2}] .

LaTeX Lean

Definition 12.23

τ

-functional

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

τ [(X_{i})_{1 \leq i \leq m}] := D [(X_{i})_{1 \leq i \leq m}] + η \sum_{i = 1}^{m} d [X_{i}; X^{0}] .

LaTeX Lean

Proposition 6.5

τ

has minimum

A pair $X_{1}, X_{2}$ of $τ$ -minimizers exist.

LaTeX Lean

Definition 6.4

τ

-minimizer

A pair of $G$ -valued random variables $X_{1}, X_{2}$ are said to be a $τ$ -minimizer if one has

τ [X_{1}; X_{2}] \leq τ [X_{1}^{'}; X_{2}^{'}]

for all $G$ -valued random variables $X_{1}^{'}, X_{2}^{'}$ .

LaTeX Lean

Proposition 12.25Existence of

τ

-minimizer

If $G$ is finite, then a $τ$ -minimizer exists.

LaTeX

Lean

multiTau_continuous
multiTau_min_exists

Definition 12.24

τ

-minimizer

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

LaTeX Lean

Proposition 12.26Minimizer close to reference variables

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

LaTeX Lean

Lemma 11.2

If $G$ is a torsion-free group and $X, Y$ are $G$ -valued random variables and $ϕ : G \to F_{2}^{d}$ is a homomorphism then

H (ϕ (X)) \leq 10 d [X; Y] .

LaTeX Lean

Lemma 11.1

If $G$ is torsion-free and $X, Y$ are $G$ -valued random variables then $d [X; 2 Y] \leq 5 d [X; Y]$ .

LaTeX Lean

Lemma 6.19Bound on distance increments

We have

\begin{aligned} \sum_{i = 1}^{2} \sum_{A \in {U, V, W}} (d [X_{i}^{0}; A | S] & - d [X_{i}^{0}; X_{i}]) \\ \leq (6 - 3 η) k + 3 (2 η k - I_{1}) . \end{aligned}

LaTeX Lean

Lemma 2.5Uniform 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$ .

LaTeX

Lean

ProbabilityTheory.exists_isUniform
ProbabilityTheory.exists_isUniform_measureSpace

Definition 2.4Uniform distribution

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

LaTeX Lean

Lemma 2.6Entropy of uniform random variable

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

LaTeX Lean

Lemma 2.7Entropy of uniform random variable, II

If $X$ is uniformly distributed on $H$ , then, then $H [X] = \log | H |$ .

LaTeX Lean

Lemma 6.18Bound on conditional mutual informations

We have

I (U : V | S) + I (V : W | S) + I (W : U | S) \leq 6 η k - \frac{1 - 5 η}{1 - η} (2 η k - I_{1}) .

LaTeX

Lean

I₃_eq
sum_condMutual_le

Lemma 2.23Vanishing of mutual information

If $X, Y$ are random variables, then $I [X : Y] = 0$ if and only if $X, Y$ are independent.

LaTeX Lean

Theorem 11.8

If $A, B \subseteq Z^{d}$ are finite non-empty sets then there exist non-empty $A^{'} \subseteq A$ and $B^{'} \subseteq B$ such that

\log \frac{| A | | B |}{| A^{'} | | B^{'} |} \leq 34 d [U_{A}; U_{B}]

such that $max (\dim A^{'}, \dim B^{'}) \leq \frac{40}{\log 2} d [U_{A}; U_{B}]$ .

LaTeX Lean

Theorem 11.10

Let $A \subseteq Z^{d}$ and $| A - A | \leq K | A |$ . There exists $A^{'} \subseteq A$ such that $| A^{'} | \geq K^{- 17} | A |$ and $\dim A^{'} \leq \frac{40}{\log 2} \log K$ .

LaTeX Lean

Theorem 11.9

If $A \subseteq Z^{d}$ is a finite non-empty set with $d [U_{A}; U_{A}] \leq \log K$ then there exists a non-empty $A^{'} \subseteq A$ such that

| A^{'} | \geq K^{- 17} | A |

and $\dim A^{'} \leq \frac{40}{\log 2} \log K$ .

LaTeX Lean

Lemma 12.44Distance bound

We have $\sum_{i = 1}^{m} d [X_{i}; Z_{2} | W] \leq 8 (m^{3} - m^{2}) k$ .

LaTeX Lean

Lemma 4.3Zero Ruzsa distance implies large symmetry group

If $X$ is a $G$ -valued random variable such that $d [X; X] = 0$ , and $x, y \in G$ are such that $P [X = x], P [X = y] > 0$ , then $x - y \in Sym [X]$ .

LaTeX Lean

Lemma 12.39Zero-sum

We have

Z_{1} + Z_{2} + Z_{3} = 0

LaTeX Lean