Uncertainty relation for smooth min- and max-entropies

Open

QAlgorithms.Papers.Independent.Intakethird100.P24.smoothEntropy_uncertainty

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $A,B,C$ be finite-dimensional nonzero quantum systems, and let $\rho_{ABC}\ge0$ satisfy $\operatorname{tr}\rho_{ABC}\le1$ . Let $\mathsf X=\{M_x\}_{x\in X}$ and $\mathsf Z=\{N_z\}_{z\in Z}$ be POVMs on $A$ with finite nonempty outcome sets. Thus all effects are positive semidefinite and each family sums to the identity. Define

c=\max_{x,z}\|\sqrt{M_x}\sqrt{N_z}\|_{\mathrm{op}}^2,\qquad q=-\log_2 c,

where the operator norm is the largest singular value. From the same input state construct

\rho_{XB}=\sum_x|x\rangle\langle x|\otimes\operatorname{tr}_{AC}[(M_x\otimes I_{BC})\rho_{ABC}],\qquad \rho_{ZC}=\sum_z|z\rangle\langle z|\otimes\operatorname{tr}_{AB}[(N_z\otimes I_{BC})\rho_{ABC}].

For every real $\varepsilon\ge0$ , the smooth conditional entropies in bits obey

H_{\min}^{\varepsilon}(X|B)_{\rho_{XB}}\ \ge\ q-H_{\max}^{\varepsilon}(Z|C)_{\rho_{ZC}}.

Smoothing ranges over all positive semidefinite operators of trace at most one on the respective joint output system, within purified distance $\varepsilon$ ; perturbations need not be classical. For subnormalized $\omega,\tau$ , that distance is $\sqrt{1-\overline F(\omega,\tau)^2}$ , where $\overline F(\omega,\tau)=\|\sqrt\omega\sqrt\tau\|_1+\sqrt{(1-\operatorname{tr}\omega)(1-\operatorname{tr}\tau)}$ . The unsmoothed min-entropy is the supremum of exponents $\lambda$ with $\rho_{AB}\le2^{-\lambda}I_A\otimes\sigma_B$ for some normalized state $\sigma_B$ ; max-entropy is its purification dual. The smooth min-entropy takes a supremum and smooth max-entropy takes an infimum over their balls.

This bounds measurement uncertainty even with distinct quantum side information and without an independence or purity assumption.

Formalization Note The order form agrees with the printed additive inequality whenever finite. If $\varepsilon\ge\sqrt{\operatorname{tr}\rho}$ , both balls contain zero, giving $H_{\min}^{\varepsilon}=+\infty$ and $H_{\max}^{\varepsilon}=-\infty$ ; the order form then reads $+\infty\ge+\infty$ . It preserves the zero input and imposes no upper bound on $\varepsilon$ .

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P24

Formal statement

noncomputable section

open scoped BigOperators ComplexConjugate Matrix ComplexOrder

namespace QAlgorithms.Papers.Independent.Intakethird100.P24

open QAlgorithms.Papers.Independent.Information100.P67
  (IsSubnormalized conditionalMinEntropy conditionalMaxEntropy
   smoothConditionalMinEntropy smoothConditionalMaxEntropyExtended)

open QAlgorithms.Papers.Independent.Dependency50.P35 (measured)

/-- Theorem 1, PDF p.2, equation (4) on p.1; general mixed-state proof on
pp.2--3. Both measured states are computed from the SAME subnormalized rho.
The extended order form is equivalent to the printed sum when finite and
reads +infinity >= +infinity when the smoothing balls contain zero.
No purity, projectivity, normalization, or epsilon < 1 premise is imposed.
At rho = 0 the source's rank-one purification shorthand is interpreted as
the zero extension (rank at most one), as required by its state domain. -/
theorem smoothEntropy_uncertainty
    {A B C X Z : Type}
    [Fintype A] [DecidableEq A] [Nonempty A]
    [Fintype B] [DecidableEq B] [Nonempty B]
    [Fintype C] [DecidableEq C] [Nonempty C]
    [Fintype X] [DecidableEq X] [Nonempty X]
    [Fintype Z] [DecidableEq Z] [Nonempty Z]
    (epsilon : ℝ) (hepsilon : 0 ≤ epsilon)
    (rho : Matrix ((A × B) × C) ((A × B) × C) ℂ)
    (hrho : IsSubnormalized rho)
    (M : X → Matrix A A ℂ) (N : Z → Matrix A A ℂ)
    (hM : IsPOVM M) (hN : IsPOVM N) :
    let rhoAC : Matrix (A × C) (A × C) ℂ :=
      fun ac ad => ∑ b : B, rho ((ac.1, b), ac.2) ((ad.1, b), ad.2)
    smoothConditionalMinEntropy (measured M (traceRight rho)) epsilon ≥
      (incompatibilityBits M N : EReal) -
        smoothConditionalMaxEntropyExtended (measured N rhoAC) epsilon := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P24

end

Source

The Uncertainty Relation for Smooth Entropies, arXiv:1009.2015v3, PDF p. 2, Theorem 1; equation (4) on PDF p.1

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $A,B,C,X,Z$ be finite nonempty sets, each with decidable equality, let $\epsilon\in\mathbb R$ satisfy $\epsilon\ge0$ , and let $\rho$ be a positive semidefinite complex matrix indexed by $(A\times B)\times C$ with $\operatorname{Re}\operatorname{Tr}\rho\le1$ , including the possibility $\rho=0$ . Let $M_x$ and $N_z$ be positive semidefinite matrices on $A$ satisfying $\sum_xM_x=I_A$ and $\sum_zN_z=I_A$ . Define the two reduced matrices by

(\rho_{AB})_{(a,b),(a',b')}=\sum_{c\in C}\rho_{((a,b),c),((a',b'),c)}, \qquad (\rho_{AC})_{(a,c),(a',c')}=\sum_{b\in B}\rho_{((a,b),c),((a',b),c')}.

Define matrices $\omega_{XB}$ and $\nu_{ZC}$ by

\begin{aligned} (\omega_{XB})_{(x,b),(x',b')} &= \begin{cases} \displaystyle\sum_{a\in A} [K_x\rho_{AB}K_x]_{(a,b),(a,b')},&x=x',\\ 0,&x\ne x', \end{cases} &K_x&=\sqrt{M_x}\otimes I_B,\\ (\nu_{ZC})_{(z,c),(z',c')} &= \begin{cases} \displaystyle\sum_{a\in A} [L_z\rho_{AC}L_z]_{(a,c),(a,c')},&z=z',\\ 0,&z\ne z', \end{cases} &L_z&=\sqrt{N_z}\otimes I_C. \end{aligned}

For a matrix $\tau$ on $J\times K$ , define the extended-real quantities

\begin{aligned} H_{\min}(\tau) &=\sup\left\{\lambda\in\mathbb R: \exists \sigma\ge0,\ \operatorname{Tr}\sigma=1,\ 2^{-\lambda}I_J\otimes\sigma-\tau\ge0\right\},\\ H_{\max}(\tau) &= \begin{cases} -\infty,&\tau=0,\\ \displaystyle\log_2\sup_{\sigma\ge0,\ \operatorname{Tr}\sigma=1} \left(\operatorname{Re}\operatorname{Tr} \sqrt{\sqrt{\tau}(I_J\otimes\sigma)\sqrt{\tau}}\right)^2,&\tau\ne0, \end{cases} \end{aligned}

where $\sigma$ is indexed by $K$ . For positive semidefinite subnormalized matrices define

P(\tau,\omega)= \sqrt{1- \left( \operatorname{Re}\operatorname{Tr}\sqrt{\sqrt{\tau}\omega\sqrt{\tau}} +\sqrt{(1-\operatorname{Re}\operatorname{Tr}\tau) (1-\operatorname{Re}\operatorname{Tr}\omega)} \right)^2}.

Here matrix square roots use real continuous functional calculus, and scalar square roots and logarithms are total real operations, with $\sqrt r=0$ for $r<0$ and $\log_2 0=0$ . Set $H_{\min}^{\epsilon}(\omega)$ to the supremum of $H_{\min}(\tau)$ , and $H_{\max}^{\epsilon}(\omega)$ to the infimum of $H_{\max}(\tau)$ , over all positive semidefinite $\tau$ on the same index set with $\operatorname{Re}\operatorname{Tr}\tau\le1$ and $P(\tau,\omega)\le\epsilon$ ; both optimizations allow $\tau=0$ . The assertion is the extended-real inequality

H_{\min}^{\epsilon}(\omega_{XB}) \ge -\log_2\!\left(\max_{x,z}\|\sqrt{M_x}\sqrt{N_z}\|_{\mathrm{op}}^2\right) - H_{\max}^{\epsilon}(\nu_{ZC}).

There is no upper bound on $\epsilon$ , and the smoothed entropies may take infinite values.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph