Quantum Information Ordering and Differential Privacy

Quantum information theory is built on entropic quantities; among them, the sandwiched Rényi relative entropy is a fundamental divergence with various applications, and its data processing inequality (DPI) under quantum channels is a cornerstone result. In this work, we present a Lean 4 library for quantum information, designed as a reusable formal infrastructure for theoretical analysis. As a central demonstration of the library, we formalize the DPI for the sandwiched Rényi relative entropy for positive semidefinite operators on finite-dimensional quantum systems. The library provides a basis-independent operator-theoretic framework for finite-dimensional quantum mechanics compatible with the standard mathematical library Mathlib, including reusable interfaces for finite-dimensional systems, states, channels, tensor products, partial traces, Choi operators, Kraus representations, and Stinespring representations. It also builds infrastructure for noncommutative trace inequalities, including operator monotonicity and convexity via the real continuous functional calculus, block-operator positivity, Hilbert-Schmidt operator spaces, Jensen's operator inequality, generalized perspectives, operator power means, and Lieb-Ando trace inequalities. On top of this framework, we formalize entropy-specific ingredients for the DPI: variational formulas for the sandwiched quasi-entropy via Young and reverse-Young inequalities, tensor-product compatibility of real powers, and Haar measures on unitary groups. Together, these components yield a Lean formalization of the DPI, give strong subadditivity as a corollary, and provide the last missing component needed to complete the Lean formalization of the generalized quantum Stein's lemma. More broadly, the development provides machine-checkable foundations for future formalized and AI-assisted research in quantum information theory.

Deep parameterized quantum circuits may remain sensitive to a parameter change while the observables retained by a learning model barely respond. We study this separation for a fixed computational-basis measurement. For a pure-state tangent, we compare the quantum Fisher information $F_Q$, the Fisher information $F_{\rm full}$ in the complete bitstring distribution, and the largest variance-normalized response $\mathcal I_{\mathcal A}$ available to a diagonal readout space $\mathcal A$. If the joint state--tangent frame is Haar random, we prove that the two successive information fractions are independent Beta variables whose means are $1/2$ and $r/(2^n-1)$, where $r$ is the centered dimension of the readout. Consequently, even the joint span of all computational-basis Pauli strings through any fixed weight $k$ retain only $O(n^k2^{-n})$ of the full-record information. Exact-statevector experiments across six circuit families show increasing finite-size agreement with this hierarchy in five nonconserving ensembles as the circuit depth grows. A number-conserving family departs strongly from the isotropic prediction even after correcting the support and readout rank, showing that rank alone is insufficient without tangent isotropy.

Federated differentially private protocols can communicate over many adaptive rounds and reuse each client's local samples. Existing lower bound arguments for federated DP are often restricted to noninteractive protocols or fresh batch decompositions, so the fundamental information-theoretic limit of estimation under fully interactive protocols remains unknown. We establish a federated van Trees inequality for parameter estimation under squared \ell_2 loss from any complete public transcript satisfying a clientwise zCDP constraint at the sample level. A scalar trace form covers homogeneous experiments, while a matrix form preserves directional Fisher geometry in heterogeneous experiments where different clients are informative in different subspaces. Together with existing upper bounds for the corresponding problems, these results identify the minimax rates for various statistical problems including mean estimation, linear regression, nonparametric regression, and functional mean estimation over the full class of interactive public-transcript protocols. For these problems, arbitrary public interaction and repeated sample reuse do not improve the rate over simpler restricted protocols. The key technical ingredient in our paper is a contraction inequality for the Fisher information in the transcript: each client's contribution is bounded both by the Fisher information in its local experiment and by its total privacy budget.