Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

A supporting functional at every pure bipartite state

Abstract

In every finite-dimensional bipartite system, each pure state admits a Hermitian supporting functional for the entanglement of formation.

Let Alice and Bob have positive dimensions a and b. Fin(a) and Fin(b) label their bases by 0 through a - 1 and 0 through b - 1: a source index (i,j) in the ranges 1 through a and 1 through b corresponds to (i - 1,j - 1) here. Vectors are functions on Fin(a) times Fin(b), and matrices have rows and columns in that same product. Both even and odd positive dimensions are included, independently on each factor.

Definition 1.1 (The supporting-functional assertion).

Formalization. D5/S3/Quantum/PureState/PureStateFormationSupportingFunctional.claim (✓ std3).

Citation. A. S. Holevo; M. E. Shirokov (2026). Log-Sobolev inequality, von Neumann entropy and Entanglement of Formation. URL: https://arxiv.org/abs/2609.12667v3.

Commentary.

Holevo and Shirokov ask in the Introduction and Section 3.1 whether the entanglement of formation has a supporting affine functional at every pure state of a finite-dimensional composite system. The assertion below uses a Hermitian matrix W to represent that functional by the real part of Tr(W sigma). On the trace-one state space this representation also includes an affine constant, by adding a scalar multiple of the identity to W.

The normalization is the squared vector norm, equivalently star(psi) dot psi = 1. rankOneDensity(psi) has entry psi(i,j) times the complex conjugate of psi(k,l). pureDensityState(psi) is the density state with that matrix; its unit-norm proof argument is supplied by the displayed normalization and suppressed in the formula. marginalRight traces out Bob and retains Alice. DensityState consists of positive semidefinite matrices of trace one, and CStarMatrix.ofMatrix.symm(val(sigma)) is the underlying matrix.

The symbol E with subscript F denotes E_F, the infimum of the average marginal entropy over all finite pure ensembles with the prescribed average state. In the entropy definition, CFC.log applies the natural real logarithm by functional calculus. Its spectral expression uses the eigenvalues of the Hermitian underlying density matrix, indexed by n; every zero eigenvalue contributes zero.

The marginal traces out Bob. The coefficient matrix M represents a joint vector, mass is its squared norm, and Pure(a,b) consists of the coefficient matrices of mass one.

An Ensemble(n,sigma) consists of probabilities p and normalized pure coefficient matrices q with the displayed average. Complex(p(i)) is the real-to-complex coercion; multiplying a matrix by this scalar denotes scalar multiplication. The lambda expression uncurries a coefficient matrix. For an ensemble e, p(e) and psi(e) are its probability and pure-vector projections. The normalization in Pure supplies the suppressed proof argument of pureDensityState.

E_F takes values in ENNReal, the extended nonnegative reals. Both infima are taken in ENNReal, and ENNReal.ofReal is applied to the whole real ensemble cost inside the infima. ENNReal.ofReal(x) is max(x,0) in that space. In the claim, it is applied to the whole real trace value in both the pure-state equality and the comparison for every sigma. The real equality with the marginal entropy is stated separately from the equality after ofReal, so the value at the pure state retains its sign information.

Theorem 1.2 (The assertion holds in all finite dimensions).

Proof. Machine-checked in Lean as D5/S3/Quantum/PureState/PureStateFormationSupportingFunctional.result (✓ std3). ∎

Resolves. Problems/holevo-shirokov-2026-pure-state-formation-supporting-functional (proved) by D5/S3/Quantum/PureState/PureStateFormationSupportingFunctional.result.

Source. Repository-derived.

Acknowledgement. A. S. Holevo; M. E. Shirokov (2026). Log-Sobolev inequality, von Neumann entropy and Entanglement of Formation. URL: https://arxiv.org/abs/2609.12667v3.

Commentary.

The construction answers the question of Holevo and Shirokov. Put P = |psi><psi| and R = Tr_B(P), and write log-zero(R) for spectral application of the real logarithm, set to zero at a zero eigenvalue. If r(i) are the eigenvalues of R, take c to be the sum of their reciprocals, with reciprocal zero at zero. Thus c is nonnegative and c r(i) is at least one whenever r(i) is positive.

For r >= 0, 0 <= t <= 1 and c >= 0 with c r >= 1 when r > 0, the scalar logarithmic inequality gives -t log-zero(r) - (t - r) - c(t - r)^2 <= -t log(t), where the right side is zero at t = 0. For positive r and t this follows from log(t/r) <= t/r - 1 and 1/r <= c. The cases r = 0 and t = 0 follow separately from nonnegativity and c r >= 1, respectively.

For any density matrix T on Alice’s space, average this scalar inequality over the two eigenbases with weights w(i,j) = |<e(i),u(j)>|^2. The overlap matrix is doubly stochastic: every row and column sums to one. The linear term cancels because both spectra sum to one, the logarithmic term becomes -Re Tr(log-zero(R) T), and the weighted squared differences become the squared Hilbert-Schmidt distance. Consequently S(T) >= -Re Tr(log-zero(R) T) - c ||T - R||_HS^2.

Cauchy-Schwarz in Bob’s index gives ||Tr_B(X)||_HS^2 <= b ||X||_HS^2 for every joint matrix X. For a pure density Q, ||Q - P||_HS^2 = 2(1 - Re Tr(PQ)). Set K = 2bc and W = -log-zero(R) tensor I_B - K(I_AB - P). This W is Hermitian. The partial-trace bound and the entropy estimate give Re Tr(WQ) <= S(Tr_B(Q)), with equality Re Tr(WP) = S(R) at Q = P.

For every finite pure ensemble with average sigma, linearity of the trace and the pure-state inequality bound Re Tr(W sigma) by its average marginal entropy. Applying ofReal and taking the infimum over all these ensembles proves the bound by E_F(sigma). At P, the one-element ensemble gives the reverse inequality, hence E_F(P) = ofReal(Re Tr(WP)). Together with the real equality at P, these are precisely the clauses of claim.

References