Global vs. Product Observables in Bipartite Quantum Systems: The Sharp Bound
Zhi Li, Xiaofei Shi
quant-ph
Aug 6, 2026 · v1
math.FA
TL;DR
The main upper bound comparing trace norm and injective tensor norm is formalized and machine-checked in Lean.
Abstract
To probe a bipartite quantum system, one may use arbitrary global operators or restrict to product operators acting separately on the two subsystems. We determine the sharp universal comparison between the resulting norms. For every $z\in M_n\otimes M_m$, we prove $\|z\|_1\leq\sqrt{2}\min\{n,m\}\|z\|_\varepsilon$, where $\|\cdot\|_1$ is the trace norm and $\|\cdot\|_\varepsilon$ is the injective tensor norm associated with the trace norms on $M_n$ and $M_m$. To prove the upper bound, we establish an $L_1$ noncommutative Khintchine inequality whose random coefficients are the entries of a Haar unitary. We also show that the coefficient $\sqrt{2}$ is sharp. As applications, we show that the same sharp constant governs the gap between bipartite correlation measured in trace norm and that measured by a correlation function, and obtain an improved universal upper bound for quantum data hiding. The upper bound has also been formalized and machine-checked in Lean.
Problem
Probing a bipartite quantum system can use arbitrary global operators or product operators acting separately on subsystems. The question is the sharp universal comparison between the resulting norms (trace norm versus injective tensor norm) as a function of local dimensions.
Approach
For z in M_n ⊗ M_m, the authors prove ||z||_1 ≤ √2 min{n,m} ||z||_ε. The upper bound is established via an L_1 noncommutative Khintchine inequality with random coefficients given by entries of a Haar unitary, combined with block-matrix trace-norm estimates. The lower bound uses a construction based on the fermionic canonical anticommutation relations (CAR). The upper bound was formalized and machine-checked in Lean, with statements manually verified against the paper.
Results
The sharp constant √2 is determined, improving prior bounds (quadratic, then min{n,m}^{3/2}, then 2 min{n,m}). The same constant governs the gap between bipartite correlation measured in trace norm versus correlation function, and yields an improved universal upper bound for quantum data hiding.
