The fully entangled fraction and the steering-ellipsoid centre

Abstract

Every two-qubit density matrix rho satisfies rho <= (2 - |c|)(1 tensor rho_B), where c is the centre of Alice’s steering ellipsoid and rho_B is Bob’s reduced state; hence its fully entangled fraction is at most 1 - |c|/2, and every value |c| = t in [0, 1] is attained by a state whose fully entangled fraction equals 1 - t/2. This proves Conjecture 2 of A. Milne, D. Jennings, S. Jevtic and T. Rudolph (arXiv:1404.3951).

Definition 1.1 (The Pauli matrices).

$$(\mathrm{pauli}\left(0\right)=\mathrm{pauliMatrix}\left(X\right))\wedge ((\mathrm{pauli}\left(1\right)=\mathrm{pauliMatrix}\left(Y\right))\wedge (\mathrm{pauli}\left(2\right)=\mathrm{pauliMatrix}\left(Z\right)))$$

Formalization. D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.pauli (✓ std3).

Citation. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

The three Pauli matrices sigma_x, sigma_y, sigma_z indexed by Fin 3. They are the Pauli matrices pauliMatrix of StabilizerPairLocalUnitaryInequivalence at the labels X, Y, Z: pauliMatrix X = qubitX = [[0, 1], [1, 0]], pauliMatrix Y = i qubitX qubitZ = [[0, -i], [i, 0]] and pauliMatrix Z = qubitZ = [[1, 0], [0, -1]]. Since Fin 3 has exactly the elements 0, 1, 2, the three displayed equations are the whole definition.

Theorem 1.2 (The first Pauli matrix).

$$D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{pauli}\left(0\right)=\left(\begin{array}{cc}0& 1\\ 1& 0\end{array}\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.pauli_zero (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

The Pauli matrix at index zero is the two-by-two matrix with zero diagonal entries and off-diagonal entries one.

Theorem 1.3 (The second Pauli matrix).

$$D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{pauli}\left(1\right)=\left(\begin{array}{cc}0& -\mathrm{Complex}.I\\ \mathrm{Complex}.I& 0\end{array}\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.pauli_one (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

The Pauli matrix at index one has zero diagonal entries, upper-right entry minus the imaginary unit and lower-left entry the imaginary unit.

Theorem 1.4 (The third Pauli matrix).

$$D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{pauli}\left(2\right)=\left(\begin{array}{cc}1& 0\\ 0& -1\end{array}\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.pauli_two (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

The Pauli matrix at index two is diagonal with entries one and minus one.

Definition 1.5 (Alice’s Bloch vector).

$$\forall rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\forall i\in \mathrm{Fin}\left(3\right),\mathrm{blochA}\left(rho,i\right)=\mathrm{re}\left(\mathrm{trace}\left(rho\cdot \mathrm{kronecker}\left(\mathrm{pauli}\left(i\right),1\right)\right)\right)$$

Formalization. D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.blochA (✓ std3).

Citation. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

A two-qubit operator is a complex matrix indexed by pairs of qubit indices, the first entry of the pair belonging to Alice and the second to Bob. Following the companion paper, Theta_{mu nu} = tr(rho sigma_mu tensor sigma_nu): Alice’s Bloch vector has components a_i = Re tr(rho (sigma_i tensor 1)), where kronecker is the Kronecker product and 1 the two-by-two identity.

Definition 1.6 (Bob’s Bloch vector).

$$\forall rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\forall j\in \mathrm{Fin}\left(3\right),\mathrm{blochB}\left(rho,j\right)=\mathrm{re}\left(\mathrm{trace}\left(rho\cdot \mathrm{kronecker}\left(1,\mathrm{pauli}\left(j\right)\right)\right)\right)$$

Formalization. D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.blochB (✓ std3).

Citation. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

Bob’s Bloch vector has components b_j = Re tr(rho (1 tensor sigma_j)).

Definition 1.7 (The correlation matrix).

$$\forall rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\forall i\in \mathrm{Fin}\left(3\right),\forall j\in \mathrm{Fin}\left(3\right),\mathrm{corr}\left(rho,i,j\right)=\mathrm{re}\left(\mathrm{trace}\left(rho\cdot \mathrm{kronecker}\left(\mathrm{pauli}\left(i\right),\mathrm{pauli}\left(j\right)\right)\right)\right)$$

Formalization. D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.corr (✓ std3).

Citation. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

The correlation matrix has entries T_ij = Re tr(rho (sigma_i tensor sigma_j)), first index Alice.

Definition 1.8 (Euclidean length).

$$\forall v\in \mathrm{Fin}\left(3\right)\to \mathbb{R},\mathrm{vlen}\left(v\right)=\sqrt{\sum _{i:\mathrm{Fin}\left(3\right)}(v{\left(i\right)}^2)}$$

Formalization. D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.vlen (✓ std3).

Citation. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

The Euclidean length of a real three-vector, the square root of the sum of the squares of its components. The scalar c of the conjecture is the length of the centre vector: the paper writes “For c = (0, 0, c)” and plots against “the magnitude of the steering ellipsoid centre”.

Definition 1.9 (The centre of the steering ellipsoid).

$$\forall rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\forall i\in \mathrm{Fin}\left(3\right),\mathrm{centre}\left(rho\right)\left(i\right)=\mathrm{ite}\left(\mathrm{vlen}\left(\mathrm{blochB}\left(rho\right)\right)=1,\mathrm{blochA}\left(rho,i\right),\frac{\mathrm{blochA}\left(rho,i\right)-{\sum }_{j:\mathrm{Fin}\left(3\right)}(\mathrm{corr}\left(rho,i,j\right)\cdot \mathrm{blochB}\left(rho,j\right))}{1-\mathrm{vlen}{\left(\mathrm{blochB}\left(rho\right)\right)}^2}\right)$$

Formalization. D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.centre (✓ std3).

Citation. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

Section I of the paper: “Given all possible measurements by Bob, the set of Bloch vectors to which Alice can be steered forms her steering ellipsoid E inside the Bloch sphere. E is described by its centre c and a real, symmetric 3 x 3 matrix Q.” The companion paper of Jevtic, Pusey, Jennings and Rudolph (PRL 113, 020402) gives the centre: “This gives a steering ellipsoid centred at c_A = (a - T b)/(1 - b^2)”, and “If b = 1 then rho is a product state in which case there is no steering and the steering ellipsoid is the single point a.” The definition takes c = (a - T b)/(1 - |b|^2) when |b| is not 1 and c = a when |b| = 1; the display states it coordinate by coordinate, with (T b)_i the sum over j of T_ij b_j.

Definition 1.10 (Maximally entangled vectors).

$$\forall e\in (\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right))\to \mathbb{C},\mathrm{IsMaxEntangled}\left(e\right)\iff ((\sum _{k:(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right))}({\Vert e\left(k\right)\Vert }^2)=1)\wedge ((\mathrm{partialTraceRight}\left(\mathrm{vecMulVec}\left(e,\mathrm{star}\left(e\right)\right)\right)=\frac{1}{2}\cdot 1)\wedge (\mathrm{partialTraceLeft}\left(\mathrm{vecMulVec}\left(e,\mathrm{star}\left(e\right)\right)\right)=\frac{1}{2}\cdot 1)))$$

Formalization. D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.IsMaxEntangled (✓ std3).

Citation. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

A two-qubit vector e is maximally entangled when it is a unit vector and both of its reduced states are half the identity: partialTraceRight traces out Bob and partialTraceLeft traces out Alice from the rank-one operator vecMulVec e (star e) = |e><e|, and (1/2) 1 is the scalar multiple of the identity. For two qubits these are exactly the vectors (U tensor V)(|00> + |11>)/sqrt 2 with U, V unitary.

Definition 1.11 (The fully entangled fraction).

$$\forall rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\mathrm{fef}\left(rho\right)=\mathrm{sSup}\left(\{f\mid \exists e\in (\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right))\to \mathbb{C},(\mathrm{IsMaxEntangled}\left(e\right))\wedge (f=\mathrm{re}\left(\mathrm{dotProduct}\left(\mathrm{star}\left(e\right),\mathrm{mulVec}\left(rho,e\right)\right)\right))\}\right)$$

Formalization. D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.fef (✓ std3).

Citation. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

Section III of the paper: “The fully entangled fraction of a bipartite state rho is defined by f(rho) = max_phi <phi| rho |phi>, where the maximum is taken over all maximally entangled states |phi>.” The definition takes the supremum of the real expectation Re <e| rho |e> = re(star e . (rho e)) over all maximally entangled e; for a density matrix the set is non-empty and bounded, and attainment of the maximum is not used.

Definition 1.12 (Conjecture 2).

$$claim\iff ((\forall rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),(\mathrm{PosSemidef}\left(rho\right))\Rightarrow \left((\mathrm{trace}\left(rho\right)=1)\Rightarrow \mathrm{fef}\left(rho\right)\le 1-\frac{\mathrm{vlen}\left(\mathrm{centre}\left(rho\right)\right)}{2}\right))\wedge (\forall t\in \mathbb{R},(0\le t)\Rightarrow \left((t\le 1)\Rightarrow \left(\exists rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),(\mathrm{PosSemidef}\left(rho\right))\wedge ((\mathrm{trace}\left(rho\right)=1)\wedge ((\mathrm{vlen}\left(\mathrm{centre}\left(rho\right)\right)=t)\wedge (\mathrm{fef}\left(rho\right)=1-\frac{t}{2})))\right)\right)))$$

Formalization. D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.claim (✓ std3).

Citation. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

Section V, Conjecture 2: “Let rho be a general two-qubit state with E centred at c. The fully entangled fraction is tightly bounded as f(rho) <= 1 - c/2.” A two-qubit state is a positive semidefinite complex 4 x 4 matrix of trace 1. The first conjunct is the bound for every state; the second makes “tightly” precise: for every t in [0, 1] there is a state with |c| = t and fully entangled fraction exactly 1 - t/2.

Definition 1.13 (Bloch coordinates of a qubit operator).

$$\forall X\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),\forall i\in \mathrm{Fin}\left(3\right),D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{blochVec}\left(X,i\right)=\mathrm{Complex}.\mathrm{re}\left(\mathrm{Matrix}.\mathrm{trace}\left(X\cdot D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{pauli}\left(i\right)\right)\right)$$

Formalization. D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.blochVec (✓ std3).

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

For any complex two-by-two matrix X, the ith Bloch coordinate is the real part of the trace of X times the ith Pauli matrix. No Hermitian or trace condition is required in this definition.

Definition 1.14 (The computational vector at zero and one).

$$\forall k\in (\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{ev}\left(k\right)=[[0,1],[0,0]]\left(\mathrm{Prod}.\mathrm{fst}\left(k\right)\right)\left(\mathrm{Prod}.\mathrm{snd}\left(k\right)\right)$$

Formalization. D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.ev (✓ std3).

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

The real vector ev has value one at the pair (0, 1) and zero at the other three pairs of qubit labels.

Theorem 1.15 (Euclidean length as a norm).

$$\forall v\in \mathrm{Fin}\left(3\right)\to \mathbb{R},D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(v\right)=\Vert (\mathrm{WithLp}.\mathrm{toLp}\left(2,v\right):\mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right))\Vert$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.vlen_eq_norm (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

The length vlen of a real three-vector equals the norm of that vector in EuclideanSpace, with WithLp.toLp 2 identifying the coordinate function with its Euclidean vector.

Theorem 1.16 (Euclidean length is nonnegative).

$$\forall v\in \mathrm{Fin}\left(3\right)\to \mathbb{R},0\le D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(v\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.vlen_nonneg (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

Every real three-vector has nonnegative Euclidean length, since its length is a real square root.

Theorem 1.17 (Tracing an Alice observable).

$$\forall rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\forall A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),\mathrm{Matrix}.\mathrm{trace}\left(rho\cdot \mathrm{Matrix}.\mathrm{kronecker}\left(A,1\right)\right)=\mathrm{Matrix}.\mathrm{trace}\left(D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{PartialTraceMutualInformation}.\mathrm{partialTraceRight}\left(rho\right)\cdot A\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.trace_mul_kron_one (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

The trace of rho times A tensor the identity equals the trace of Alice’s reduced operator times A. This identity holds for arbitrary complex operators, without positivity or normalization assumptions.

Theorem 1.18 (Tracing a Bob observable).

$$\forall rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\forall B\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),\mathrm{Matrix}.\mathrm{trace}\left(rho\cdot \mathrm{Matrix}.\mathrm{kronecker}\left(1,B\right)\right)=\mathrm{Matrix}.\mathrm{trace}\left(D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{PartialTraceMutualInformation}.\mathrm{partialTraceLeft}\left(rho\right)\cdot B\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.trace_mul_one_kron (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

The trace of rho times the identity tensor B equals the trace of Bob’s reduced operator times B. This identity holds for arbitrary complex operators, without positivity or normalization assumptions.

Theorem 1.19 (Moving a local filter across the trace).

$$\forall K\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),\forall A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),\forall rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\mathrm{Matrix}.\mathrm{trace}\left(\mathrm{Matrix}.\mathrm{kronecker}\left(1,K\right)\cdot rho\cdot \mathrm{Matrix}.\mathrm{conjTranspose}\left(\mathrm{Matrix}.\mathrm{kronecker}\left(1,K\right)\right)\cdot \mathrm{Matrix}.\mathrm{kronecker}\left(A,1\right)\right)=\mathrm{Matrix}.\mathrm{trace}\left(rho\cdot \mathrm{Matrix}.\mathrm{kronecker}\left(A,\mathrm{Matrix}.\mathrm{conjTranspose}\left(K\right)\cdot K\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.trace_conj_kron (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

For arbitrary complex two-by-two matrices K and A and a complex two-qubit operator rho, the trace of the operator filtered by the identity tensor K against A tensor the identity equals the trace of rho against A tensor K adjoint times K. This follows from cyclicity of the trace and multiplication of Kronecker products.

Theorem 1.20 (The Kronecker product distributes over subtraction).

$$\forall A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),\forall X\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),\forall Y\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),\mathrm{Matrix}.\mathrm{kronecker}\left(A,X-Y\right)=\mathrm{Matrix}.\mathrm{kronecker}\left(A,X\right)-\mathrm{Matrix}.\mathrm{kronecker}\left(A,Y\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.kron_sub (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

For arbitrary complex two-by-two matrices A, X and Y, A tensor (X minus Y) equals A tensor X minus A tensor Y.

Theorem 1.21 (Length on the third coordinate axis).

$$\forall s\in \mathbb{R},D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left([0,0,s]\right)=\left|s\right|$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.vlen_e3 (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

For every real s, the Euclidean length of (0, 0, s) is the absolute value of s.

Theorem 1.22 (Agreement of Hermitian Bloch coordinates).

$$\forall Z\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),(\mathrm{Matrix}.\mathrm{IsHermitian}\left(Z\right))\Rightarrow (\mathrm{WithLp}.\mathrm{toLp}\left(2,D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{blochVec}\left(Z\right)\right):\mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right))=D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{ActualPureQubitCostInfimum}.\mathrm{bloch}\left(Z\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.blochVec_eq_bloch (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

For every Hermitian complex two-by-two matrix Z, the coordinates blochVec Z, regarded as a Euclidean vector, equal the Bloch vector bloch Z of ActualPureQubitCostInfimum.

Theorem 1.23 (A canonical state and a reverse Bob filter).

$$\forall rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),(\mathrm{Matrix}.\mathrm{PosSemidef}\left(rho\right))\Rightarrow \left((\mathrm{Matrix}.\mathrm{trace}\left(rho\right)=1)\Rightarrow \left((D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{blochB}\left(rho\right)\right)<1)\Rightarrow \left(\exists sigma\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\exists F\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),(\mathrm{Matrix}.\mathrm{PosSemidef}\left(sigma\right))\wedge ((D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{PartialTraceMutualInformation}.\mathrm{partialTraceLeft}\left(sigma\right)=(\frac{1}{2})\cdot (1))\wedge ((D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{blochA}\left(sigma\right)=D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{centre}\left(rho\right))\wedge ((rho=\mathrm{Matrix}.\mathrm{kronecker}\left(1,F\right)\cdot sigma\cdot \mathrm{Matrix}.\mathrm{conjTranspose}\left(\mathrm{Matrix}.\mathrm{kronecker}\left(1,F\right)\right))\wedge ((F\cdot \mathrm{Matrix}.\mathrm{conjTranspose}\left(F\right)=(2)\cdot (D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{PartialTraceMutualInformation}.\mathrm{partialTraceLeft}\left(rho\right)))\wedge (\mathrm{Complex}.\mathrm{normSq}\left(\mathrm{Matrix}.\det \left(F\right)\right)=1-D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}{\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{blochB}\left(rho\right)\right)}^2)))))\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.canonical_filter (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

Let rho be positive semidefinite with trace one and Bob Bloch length strictly less than one. There are a positive semidefinite two-qubit operator sigma with Bob marginal half the identity and Alice Bloch vector equal to centre rho, and a complex two-by-two filter F which reconstructs rho from sigma. The filter satisfies F F adjoint = 2 rho_B, and the squared complex norm of its determinant is 1 minus the squared Bob Bloch length.

Theorem 1.24 (Normalization from the Bob marginal).

$$\forall sigma\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),(D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{PartialTraceMutualInformation}.\mathrm{partialTraceLeft}\left(sigma\right)=(\frac{1}{2})\cdot (1))\Rightarrow \mathrm{Matrix}.\mathrm{trace}\left(sigma\right)=1$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.canonical_trace (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

Every complex two-qubit operator whose Bob marginal is half the identity has trace one. Positivity is not required for this trace identity.

Theorem 1.25 (States with a maximally mixed Bob marginal).

$$\forall sigma\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),(\mathrm{PosSemidef}\left(sigma\right))\Rightarrow \left((\mathrm{partialTraceLeft}\left(sigma\right)=\frac{1}{2}\cdot 1)\Rightarrow \left(\forall phi\in (\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right))\to \mathbb{C},\mathrm{re}\left(\mathrm{dotProduct}\left(\mathrm{star}\left(phi\right),\mathrm{mulVec}\left(sigma,phi\right)\right)\right)\le (1-\frac{\mathrm{vlen}\left(\mathrm{blochA}\left(sigma\right)\right)}{2})\cdot \mathrm{re}\left(\mathrm{dotProduct}\left(\mathrm{star}\left(phi\right),phi\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.canonical_bound (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

Let sigma be positive semidefinite with Bob marginal sigma_B = 1/2 (so its trace is 1), let a be the Bloch vector of its Alice marginal sigma_A, and let phi be a vector with t = <phi| sigma |phi> > 0. Put w = sigma phi. The Cauchy-Schwarz inequality for the positive form of sigma gives sigma >= w w^H / t and t^2 <= |phi|^2 |w|^2. For a two-by-two Hermitian X let rad X be the length of its Bloch vector, the difference of its eigenvalues; it is a seminorm, rad(sigma_A) = |a|, and rad Z <= tr Z for positive semidefinite Z because det Z >= 0. Taking Bob’s marginal of sigma - w w^H / t gives 1/2 - tr_A(w w^H)/t >= 0, hence rad(tr_A w w^H)/t <= 1 - |w|^2/t. The two marginals of the rank-one operator w w^H have the same trace |w|^2 and the same determinant |det W|^2, W the coefficient matrix of w, so they have the same rad. Taking Alice’s marginal, sigma_A = tr_B(w w^H)/t + Z with Z >= 0 and tr Z = 1 - |w|^2/t, so |a| <= rad(tr_B w w^H)/t + tr Z <= 2 - 2|w|^2/t <= 2 - 2t/|phi|^2. This is the bound; for t = 0 it follows from |a| <= 1.

Theorem 1.26 (The operator inequality).

$$\forall rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),(\mathrm{PosSemidef}\left(rho\right))\Rightarrow \left((\mathrm{trace}\left(rho\right)=1)\Rightarrow \left(\forall x\in (\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right))\to \mathbb{C},\mathrm{re}\left(\mathrm{dotProduct}\left(\mathrm{star}\left(x\right),\mathrm{mulVec}\left(rho,x\right)\right)\right)\le (2-\mathrm{vlen}\left(\mathrm{centre}\left(rho\right)\right))\cdot \mathrm{re}\left(\mathrm{dotProduct}\left(\mathrm{star}\left(x\right),\mathrm{mulVec}\left(\mathrm{kronecker}\left(1,\mathrm{partialTraceLeft}\left(rho\right)\right),x\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.operator_bound (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

Let rho be a two-qubit density matrix with Bob marginal rho_B = [[p, q], [conj q, r]] and Bloch vector b, so that 1 - |b|^2 = 4d with d = pr - |q|^2 = det rho_B. If |b| < 1 then d > 0 and p > 0; with u = sqrt d the filters H = [[u, 0], [-conj q, p]] and G = [[p, 0], [conj q, u]] satisfy H rho_B H^H = p d 1, G H = p u 1, G G^H = p rho_B and H^H H = p (1 - rho_B). The filtered operator sigma = (1 tensor H) rho (1 tensor H)^H / (2 p d) is positive semidefinite with Bob marginal 1/2, and since 2(1 - rho_B) = 1 - b . sigma its Alice Bloch vector is (a - T b)/(1 - |b|^2) = c. Moreover rho = (2/p)(1 tensor G) sigma (1 tensor G)^H, so for y = (1 tensor G)^H x the bound for sigma gives Re <x| rho |x> = (2/p) Re <y| sigma |y> <= (2/p)(1 - |c|/2) p <x| 1 tensor rho_B |x>. If |b| = 1 then c = a and |a| <= 1, and it suffices to show Re <x| rho |x> <= <x| 1 tensor rho_B |x>: with t = <x| rho |x> > 0 and w = rho x, the Cauchy-Schwarz bound rho >= w w^H / t gives rho_B >= tr_A(w w^H)/t, and rad(rho_B) = tr rho_B = 1 forces rad = tr for tr_A(w w^H), so det W = 0. Then A = W conj(X)^T is a rank-one two-by-two matrix with tr A = <x|w> = t, and |tr A|^2 <= sum |A_ik|^2 = tr(tr_A(w w^H) tr_A(x x^H)) <= t tr(rho_B tr_A(x x^H)) = t <x| 1 tensor rho_B |x>.

Theorem 1.27 (Proof of the conjecture).

$$(\forall rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),(\mathrm{PosSemidef}\left(rho\right))\Rightarrow \left((\mathrm{trace}\left(rho\right)=1)\Rightarrow \mathrm{fef}\left(rho\right)\le 1-\frac{\mathrm{vlen}\left(\mathrm{centre}\left(rho\right)\right)}{2}\right))\wedge (\forall t\in \mathbb{R},(0\le t)\Rightarrow \left((t\le 1)\Rightarrow \left(\exists rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),(\mathrm{PosSemidef}\left(rho\right))\wedge ((\mathrm{trace}\left(rho\right)=1)\wedge ((\mathrm{vlen}\left(\mathrm{centre}\left(rho\right)\right)=t)\wedge (\mathrm{fef}\left(rho\right)=1-\frac{t}{2})))\right)\right))$$

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

Resolves. Problems/milne-jennings-jevtic-rudolph-2014-fully-entangled-fraction (proved) by D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.result.

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

For a maximally entangled e the reduced state tr_A(e e^H) is 1/2, so <e| 1 tensor rho_B |e> = tr(rho_B)/2 = 1/2, and the operator inequality gives Re <e| rho |e> <= (2 - |c|)/2 = 1 - |c|/2; the vector ((1 + i)/2)(|00> + |11>), a phase multiple of (|00> + |11>)/sqrt 2, is maximally entangled, so the supremum is at most 1 - |c|/2. For tightness let 0 <= t <= 1, chi = |00> + (1 - t)|11> and rho_t = (|chi><chi| + t(1 - t)|01><01|)/(2 - t), a density matrix. Its Bloch data are a = (0, 0, t(3 - 2t)/(2 - t)), b = (0, 0, t/(2 - t)), T_xz = T_yz = 0 and T_zz = (2 - 3t + 2t^2)/(2 - t). For t < 1 one has |b| < 1 and c = (a - T b)/(1 - |b|^2) = (0, 0, t); for t = 1 the state is |00><00|, |b| = 1 and c = a = (0, 0, 1). In both cases |c| = t, and the phase multiple of (|00> + |11>)/sqrt 2 gives Re <e| rho_t |e> = (1 + 2(1 - t) + (1 - t)^2)/(2(2 - t)) = 1 - t/2, which together with the bound fixes the supremum.

References

• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.IsMaxEntangled
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.blochA
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.blochB
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.blochVec
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.blochVec_eq_bloch
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.canonical_bound
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.canonical_filter
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.canonical_trace
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.centre
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.claim
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.corr
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.ev
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.fef
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.kron_sub
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.operator_bound
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.pauli
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.pauli_one
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.pauli_two
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.pauli_zero
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.result
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.trace_conj_kron
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.trace_mul_kron_one
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.trace_mul_one_kron
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.vlen
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.vlen_e3
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.vlen_eq_norm
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction.vlen_nonneg
• Dependency: D5/S3/Quantum/Divergence/ConditionalHockeyStickOrthogonalReduction
• Dependency: D5/S3/Quantum/FiniteDimensional
• Dependency: D5/S3/Quantum/Information/ActualPureQubitGeometry
• Dependency: D5/S3/Quantum/Information/PartialTraceMutualInformation
• Dependency: D5/S3/Quantum/Information/StabilizerPairLocalUnitaryInequivalence
• Dependency: D5/S3/QuantumBounds/CHSHWitness