Convexity, roof attainment and squared-concurrence comparison

Open

QAlgorithms.Papers.Independent.Intakethird100.P21.convexity_and_comparison

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

prove2quantum

Let $\rho,\sigma$ be density operators on any fixed bipartite system with positive finite local dimensions and let $p\in[0,1]$ . Write $C$ for mixed I-concurrence and $\tau$ for the separate pure-tangle convex roof. Each of $E=C$ , $E=C^2$ , and $E=\tau$ satisfies

E(p\rho+(1-p)\sigma)\le pE(\rho)+(1-p)E(\sigma), \qquad 0\le C(\rho),\qquad C(\rho)^2\le\tau(\rho).

For each $\rho$ there is a finite normalized pure-state ensemble representing $\rho$ that attains $C(\rho)$ as its average pure concurrence, and there is such an ensemble attaining $\tau(\rho)$ as its average pure tangle. The two optimizing ensembles need not coincide.

This records the minimum convention of the roofs and distinguishes convexity of squared concurrence from the source's unasserted LOCC monotonicity of that square.

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.5, Section 2, and p.3, (1.4)--(1.5): convexity of concurrence,
its square and tangle; C(rho)^2<=tau(rho); both roofs attain their minima.
No LOCC claim is made for squared mixed concurrence. -/
theorem convexity_and_comparison :
    Frontier30.P30.IsConvex (fun _ _ rho => concurrence rho) ∧
    Frontier30.P30.IsConvex (fun _ _ rho => concurrence rho ^ 2) ∧
    Frontier30.P30.IsConvex (fun _ _ rho => tangle rho) ∧
    ∀ a b : ℕ, ∀ ha : 0 < a, ∀ hb : 0 < b,
      ∀ rho : Matrix (Fin a × Fin b) (Fin a × Fin b) ℂ, IsDensityMatrix rho →
        0 ≤ concurrence rho ∧ concurrence rho ^ 2 ≤ tangle rho ∧
        (∃ e : PureEnsemble (Fin a × Fin b), IsOptimalPureEnsemble pureConcurrence rho e) ∧
        (∃ e : PureEnsemble (Fin a × Fin b), IsOptimalPureEnsemble pureTangle rho e) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P21

end

Source

I-concurrence and tangle for isotropic states, arXiv:quant-ph/0208002v1, PDF p. 5, §2: convexity and squared-concurrence versus tangle

Read-back

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

For unit vectors $\psi$ in any finite bipartite space, put $T_0(\psi)=2(1-\operatorname{Re}\operatorname{tr}((\operatorname{Tr}_2|\psi\rangle\langle\psi|)^2))$ and $C_0(\psi)=\sqrt{T_0(\psi)}$ , and let $T(\rho)$ and $C(\rho)$ be the respective infima of weighted costs over finite unit-vector decompositions $\rho=\sum_iw_i|\psi_i\rangle\langle\psi_i|$ , where $w_i\ge0$ and $\sum_iw_i=1$ . In every pair of positive natural dimensions $a,b$ , each of the three functions $C$ , $C^2$ , and $T$ satisfies

E(p\rho+(1-p)\sigma)\le pE(\rho)+(1-p)E(\sigma)

for all density matrices $\rho,\sigma$ and all real $p\in[0,1]$ . Moreover, for every density matrix $\rho$ in these dimensions,

0\le C(\rho),\qquad C(\rho)^2\le T(\rho).

There exists a finite unit-vector decomposition of $\rho$ whose weighted $C_0$ -cost equals $C(\rho)$ , and there exists a possibly different such decomposition whose weighted $T_0$ -cost equals $T(\rho)$ . Zero weights and dimensions equal to $1$ are allowed; no uniqueness, common optimizing ensemble, or bound on the number of terms is asserted.

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