Security and QKD / Theorem

Privacy amplification extractable-randomness bounds

Theorem statement

Let $\rho_{ZE}$ be a subnormalized classical--quantum state on $ZE$, classical on $Z$ with side information $E$, and let $0<\varepsilon<1$. For any $0<\delta<\varepsilon$, set $\varepsilon'=(\varepsilon-\delta)/2$, $\varepsilon''=\sqrt{2\varepsilon-\varepsilon^2}$, and \[ L := H_{\min}^{\varepsilon'}(Z|E)_{\rho}-2\log_2\frac{1}{\delta}. \] In the strict finite-alphabet convention, where output alphabet sizes are integers, the extractable-randomness length satisfies \[ \log_2 \max\{1,\lfloor 2^L\rfloor\} \le \log_2 \ell^{\varepsilon}(Z|E)_{\rho} \le H_{\min}^{\varepsilon''}(Z|E)_{\rho}. \]

Copy a short prompt with the import, Lean declaration, citations, and public source link.

Open Lean source