Mission

A Generalization of Quantum Stein's LemmaResearch Paper

Motivation

We present a generalization of quantum Stein's Lemma to the situation in which the alternative hypothesis is formed by a family of states, which can moreover be non-i.i.d.. We consider sets of states which satisfy a few natural properties, the most important being the closedness under permutations of the copies. We then determine the error rate function in a very similar fashion to quantum Stein's Lemma, in terms of the quantum relative entropy. Our result has two applications to entanglement theory. First it gives an operational meaning to an entanglement measure known as regularized relative entropy of entanglement. Second, it shows that this measure is faithful, being strictly positive on every entangled state. This implies, in particular, that whenever a multipartite state can be asymptotically converted into another entangled state by local operations and classical communication, the rate of conversion must be non-zero. Therefore, the operational definition of multipartite entanglement is equivalent to its mathematical definition.

This mission is the statement-level formalization of A Generalization of Quantum Stein's Lemma (arXiv:0904.0281v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

21 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem I: generalized state-set quantum Stein lemma, direct and strong converse (Theorem I: generalized state-set quantum Stein lemma, direct and strong converse, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

1 results of the paper are not stated yet, because the library lacks an interface they need:

§IV, unnumbered assertion: one-way-undistillable alternatives: A consistently specified extension level and communication direction for the one-way-undistillable inclusion on PDF p.28. (source-ambiguity)

Selected references

A Generalization of Quantum Stein's Lemma, arXiv:0904.0281v3, https://arxiv.org/abs/0904.0281v3

Goal · Theorem I: generalized state-set quantum Stein lemma, direct and strong converse

OPEN

noncomputable section

namespace QAlgorithms.Papers.Independent.Intake100.P63

open QAlgorithms Filter Topology

open QAlgorithms.Papers.Independent.Information100.P60 (Mat relativeBits)

open QAlgorithms.Papers.Independent.Information100.P07 (positivePart)

open QAlgorithms.Papers.Independent.Information100.P21 (Vec)

open QAlgorithms.Papers.Independent.Gap48.P20 (Copies)

open QAlgorithms.Papers.Independent.Advance50.P30 (joinCopies defectTensor)

open QAlgorithms.Papers.Independent.Information100.P69 (permute)

open scoped Matrix ComplexConjugate ENNReal ComplexOrder

attribute [local instance] Classical.propDecidable Classical.decEq

/-- PDF p.5 Theorem I, Eqs.(11)--(14): direct and strong-converse clauses. -/
theorem generalized_stein {I : Type*} [Fintype I] [DecidableEq I] [Nonempty I]
    (M : (n : ℕ) → Set (Mat (Copies I n))) (hM : stateSetAxioms M)
    (rho : Mat I) (hrho : IsDensityMatrix rho) : SteinClauses M rho := by sorry

end QAlgorithms.Papers.Independent.Intake100.P63

end

Let $H$ be a nonzero finite-dimensional complex Hilbert space and let $\rho\in\mathcal D(H)$ be a normalized density operator. For each positive integer $n$ , let $M_n\subseteq\mathcal D(H^{\otimes n})$ be closed and convex. Assume that one fixed full-rank state $\sigma$ has $\sigma^{\otimes n}\in M_n$ for every positive $n$ , that every single-copy partial trace preserves the family, that tensor products map $M_n\times M_m$ into $M_{n+m}$ , and that conjugation by every copy permutation preserves $M_n$ . Define $E_{M_n}(\xi)=\inf_{\omega\in M_n}D_2(\xi\Vert\omega)$ , using base-two relative entropy with value $+\infty$ on failed support inclusion, and define $E_M^\infty(\rho)=\inf_{n\ge1}E_{M_n}(\rho^{\otimes n})/n$ .

For a two-outcome effect $0\le A_n\le I$ , set $\alpha_n=\operatorname{Tr}[(I-A_n)\rho^{\otimes n}]$ and $b_n(\omega)=-\log_2\operatorname{Tr}(A_n\omega)/n$ , with $-\log_2 0=+\infty$ .

For every $\eta>0$ there is one effect sequence, chosen before the alternatives, such that

\alpha_n\longrightarrow0,\qquad b_n(\omega_n)+\eta\ge E_M^\infty(\rho)\quad(\forall n\ge1,\ \forall\omega_n\in M_n).

Conversely, for every $\eta>0$ and every effect sequence satisfying

b_n(\omega_n)-\eta\ge E_M^\infty(\rho)\quad(\forall n\ge1,\ \forall\omega_n\in M_n),

one has $\alpha_n\longrightarrow1$ .

This gives the direct and strong-converse operational meaning of the regularized state-set relative entropy.

Frontier · Open leaf nodes

Recent activity

Mission

A Generalization of Quantum Stein's Lemma

Goal

Frontier · Open leaf nodes

Recent activity

A Generalization of Quantum Stein's LemmaResearch Paper

Motivation

What is formalized

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Deferred results

1 results of the paper are not stated yet, because the library lacks an interface they need:

§IV, unnumbered assertion: one-way-undistillable alternatives: A consistently specified extension level and communication direction for the one-way-undistillable inclusion on PDF p.28. (source-ambiguity)

Selected references

A Generalization of Quantum Stein's Lemma, arXiv:0904.0281v3, https://arxiv.org/abs/0904.0281v3

noncomputable section namespace QAlgorithms.Papers.Independent.Intake100.P63 open QAlgorithms Filter Topology open QAlgorithms.Papers.Independent.Information100.P60 (Mat relativeBits) open QAlgorithms.Papers.Independent.Information100.P07 (positivePart) open QAlgorithms.Papers.Independent.Information100.P21 (Vec) open QAlgorithms.Papers.Independent.Gap48.P20 (Copies) open QAlgorithms.Papers.Independent.Advance50.P30 (joinCopies defectTensor) open QAlgorithms.Papers.Independent.Information100.P69 (permute) open scoped Matrix ComplexConjugate ENNReal ComplexOrder attribute [local instance] Classical.propDecidable Classical.decEq /-- PDF p.5 Theorem I, Eqs.(11)--(14): direct and strong-converse clauses. -/ theorem generalized_stein {I : Type*} [Fintype I] [DecidableEq I] [Nonempty I] (M : (n : ℕ) → Set (Mat (Copies I n))) (hM : stateSetAxioms M) (rho : Mat I) (hrho : IsDensityMatrix rho) : SteinClauses M rho := by sorry end QAlgorithms.Papers.Independent.Intake100.P63 end