Papers With

← All papers
First page of Second-Order Expansion of Privacy Amplification Under f-Divergence Criteria

Second-Order Expansion of Privacy Amplification Under f-Divergence Criteria

Mario Berta, Hao-Chung Cheng, Marco Tomamichel

cs.IT Sep 10, 2026 · v1
formalization mathlib probability cryptography
Read PDF arXiv abstract Code
TL;DR
Every numbered result and definition has a corresponding kernel-checked declaration in an accompanying Lean 4 and Mathlib development, with no project-specific axioms.
Abstract
We derive the second-order asymptotics of randomness extraction from memoryless sources with side information under security criteria based on a broad class of Csiszàr f-divergences, treating both a fixed reference side-information marginal and optimization over that marginal. The conditional varentropy decomposes into fluctuations of the conditional entropy across different values of the side information and the average variance of the conditional surprisal for each value. Without marginal optimization, these contributions yield a Gaussian-mixture second-order profile. With marginal optimization, they combine into the total conditional varentropy, yielding a single Gaussian profile. As corollaries, we obtain second-order expansions for Rényi-entropy criteria of all orders $α\in (0,1)$ and recover the known expansion for total variation distance.
Problem

Characterize the second-order asymptotics of randomness extraction (privacy amplification) from memoryless sources with side information, under security criteria given by a broad class of Csiszár f-divergences. Two settings are treated: a fixed reference side-information marginal and a reference marginal optimized over.

Approach

One-shot converse and achievability bounds reduce the leakage to a capped f-divergence perspective cost. This cost is solved by a conditional water-filling optimizer that is universal over the admissible generators. Berry–Esseen-based conditional Gaussian limits then evaluate the bounds, with two-universal hashing used for achievability. All numbered results and definitions are formalized in Lean 4 with Mathlib.

Results

With a fixed marginal, the limit is a Gaussian-mixture profile that depends separately on the conditional entropy fluctuation V1 and the average conditional variance V2. With an optimized marginal, these combine into a single Gaussian profile in the total varentropy V. Corollaries give second-order expansions for Rényi criteria of all orders α∈(0,1) and recover the known total-variation expansion.