Pure-state fidelity bound with the support-qualified equality case

Open

QAlgorithms.Papers.Independent.Intakethird100.P21.fidelity_maximization

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

prove2quantum

Let $d\ge2$ , let $\mu_1,\ldots,\mu_d\ge0$ sum to one, and let $U_A,U_B$ be local unitaries. Put $V=U_A^T U_B$ , $\Phi_d=d^{-1/2}\sum_k|k,k\rangle$ , and $\psi=(U_A\otimes U_B)\sum_k\sqrt{\mu_k}|k,k\rangle$ . The squared overlap satisfies

\langle\Phi_d|\psi\rangle\langle\psi|\Phi_d\rangle =F(\mu,V):=\frac1d\left|\sum_k\sqrt{\mu_k}V_{kk}\right|^2 \le F(\mu,I).

Equality holds exactly when there exists a common complex phase $z$ , $|z|=1$ , such that $V_{kk}=z$ for every $k$ with $\mu_k>0$ . With full Schmidt support this is equivalent to $V=zI$ .

This supplies the fidelity maximization used in the scalar reduction. The product order and support qualifier correct the printed prose; the inequality retains zero Schmidt probabilities.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P21

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P21

open scoped Matrix ComplexConjugate

open Filter

open QAlgorithms

open QAlgorithms.Papers.Independent.Information100.P03
  (PureEnsemble convexRoof pureConcurrence concurrence SchmidtData schmidtVector)

attribute [local instance] Classical.propDecidable Classical.decEq

/-- PDF p.6, (3.6)--(3.7), corrected: V=UA-transpose times UB.
Printed unrestricted equality iff V is scalar fails for zero Schmidt probabilities;
the common phase is required exactly on their positive support. -/
theorem fidelity_maximization (d : ℕ) (hd : 2 ≤ d) (mu : SchmidtProbabilities d)
    (UA UB : Matrix.unitaryGroup (Fin d) ℂ) :
    let V := (UA : Matrix (Fin d) (Fin d) ℂ)ᵀ * (UB : Matrix (Fin d) (Fin d) ℂ)
    maximallyEntangledOverlap (pureDensity (act (Matrix.kronecker (UA : Matrix (Fin d) (Fin d) ℂ)
      (UB : Matrix (Fin d) (Fin d) ℂ)) (canonicalVector mu))) = fidelityProfile mu V ∧
    fidelityProfile mu V ≤ fidelityProfile mu 1 ∧
    (fidelityProfile mu V = fidelityProfile mu 1 ↔
      ∃ z : ℂ, ‖z‖ = 1 ∧ ∀ k, 0 < mu.probability k → V k k = z) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P21

end

Source

I-concurrence and tangle for isotropic states, arXiv:quant-ph/0208002v1, PDF p. 6, §3.1, (3.6)–(3.7): pure-state fidelity bound and its equality condition

Read-back

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

For every natural number $d\ge2$ , every collection $\mu_0,\ldots,\mu_{d-1}\ge0$ summing to $1$ , and every pair of unitary complex $d\times d$ matrices $U_A,U_B$ , let

\psi_\mu=\sum_{k<d}\sqrt{\mu_k}|k,k\rangle,\qquad \Phi_d=\frac1{\sqrt d}\sum_{k<d}|k,k\rangle,\qquad V=U_A^{\mathsf T}U_B.

Then, with $\psi=(U_A\otimes U_B)\psi_\mu$ ,

\operatorname{Re}\operatorname{tr} \bigl(|\Phi_d\rangle\langle\Phi_d|\,|\psi\rangle\langle\psi|\bigr) =\frac{\left|\sum_{k<d}\sqrt{\mu_k}\,V_{kk}\right|^2}{d} \le\frac{\left(\sum_{k<d}\sqrt{\mu_k}\right)^2}{d}.

Equality in the displayed inequality holds if and only if there exists a complex number $z$ with $|z|=1$ such that $V_{kk}=z$ for every $k$ with $\mu_k>0$ . Zero probabilities are allowed, and the equality condition imposes no diagonal-entry requirement at those indices.

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