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}.
\]
Sources
- Quantum Information Processing with Finite Resources -- Mathematical Foundations
Marco Tomamichel, 2015
Lean context
Copy a short prompt with the import, Lean declaration, citations, and public source link.