The Theorem

Two correlated random variables $X$ and $Y$ take values in finite sets $\mathcal{X}$ and $\mathcal{Y}$. In privacy amplification $X$ is a string that Alice and Bob share and $Y$ is what an eavesdropper knows about it. The theorem bounds how much collision entropy $X$ loses when the value of $Y$ becomes known: for any real $s$, except with probability at most $2^{-s}$, the loss is at most $2\log_2|\mathcal{Y}| + 2s$, where $|\mathcal{Y}|$ is the number of values $Y$ can take.

Joint Distributions

A joint distribution $p$ of $X$ and $Y$ is a function on $\mathcal{X} \times \mathcal{Y}$ whose values $p(x,y)$ are nonnegative and sum to one. The first marginal $p_X$ of $p$ is the distribution of $X$ alone, obtained by summing out $Y$, $$p_X(x) = \sum_{y \in \mathcal{Y}} p(x,y),$$(1)^✦ and the second marginal $p_Y$ of $p$ is the distribution of $Y$ alone, obtained by summing out $X$, $$p_Y(y) = \sum_{x \in \mathcal{X}} p(x,y).$$(2)^✦

For a value $u$ of $Y$, the conditional distribution $p(\cdot \mid u)$ of $X$ given $Y = u$ is the function on $\mathcal{X}$ that divides each joint weight at $u$ by the weight of $u$: $$p(x \mid u) = \frac{p(x,u)}{p_Y(u)}.$$(3)^✦

Collision Entropy

The collision probability $P_c(q)$ of a distribution $q$ on a finite set $\mathcal{S}$ is the sum of the squares of its weights, $$P_c(q) = \sum_{i \in \mathcal{S}} q(i)^2 ,$$(4)^✦ the probability that two independent draws from $q$ give the same point. The collision entropy $H_c(q)$ of $q$ is the negative base two logarithm of its collision probability, $$H_c(q) = -\log_2 P_c(q),$$(5)^✦ and the collision entropy $H_c(X)$ of $X$ is that of its marginal, $H_c(p_X)$.

The conditional collision entropy $H_c(X \mid Y = u)$ of $X$ given $Y = u$ is the collision entropy of the conditional distribution (3): $$H_c(X \mid Y = u) = H_c\bigl(p(\cdot \mid u)\bigr) = -\log_2 \sum_{x \in \mathcal{X}} p(x \mid u)^2 .$$(6)^✦

The Claim

What Is Checked

The claim is stated over a joint distribution of $X$ and $Y$ on two finite sets, the collision entropies of its first marginal and of its conditional distributions, (5) and (6), and the weights of its second marginal (2).

About these constructions the library proves the bound (7).