AI 中文总结
该研究针对二分量子系统，确定了全局算子与乘积算子的迹范数和内射张量范数间的精确边界，建立相关不等式并应用于量子数据隐藏，且结果已在 Lean 中形式化验证。
AI 中文摘要
为探测二分量子系统，可使用任意全局算子或限制为分别作用于两个子系统的乘积算子。我们确定了所得范数之间的精确通用比较关系。对任意 $z\in M_n\otimes M_m$，证明 $\\|z\\|_1\leq\sqrt{2}\min\{n,m\}\\|z\\|_\varepsilon$，其中 $\\|\cdot\\|_1$ 为迹范数，$\\|\cdot\\|_\varepsilon$ 为与 $M_n$ 和 $M_m$ 上迹范数相关的内射张量范数。为证明上界，建立了 $L_1$ 非交换 Khintchine 不等式，其随机系数为哈尔幺正矩阵的元素，还证明系数 $\sqrt{2}$ 是精确的。作为应用，表明相同精确常数决定了迹范数测量的二分关联与关联函数测量的关联之间的间隙，并得到量子数据隐藏的改进通用上界。该上界已在 Lean 中形式化并经过机器验证。
英文摘要
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.
