Relative entropy coherence is at most l1 coherence

Abstract

The l1 norm of coherence bounds relative entropy coherence in every finite dimension.

Definition 1.1 (Density matrices).

$$\forall (n:\mathbb{N}),\forall (rho:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),\mathrm{IsState}\left(rho\right)\iff \left((\mathrm{PosSemidef}\left(rho\right))\wedge (\mathrm{trace}\left(rho\right)=1)\right)$$

Formalization. D5/S3/Divergence/CoherenceL1RelativeEntropyBound.IsState (✓ std3).

Citation. Swapan Rana, Preeti Parashar, Maciej Lewenstein (2016). Trace-distance measure of coherence. DOI: 10.1103/PhysRevA.93.012110. URL: https://arxiv.org/abs/1511.01854v2.

Commentary.

A complex matrix is a quantum state exactly when it is positive semidefinite and has trace one.

Definition 1.2 (Base-2 von Neumann entropy).

$$\forall (n:\mathbb{N}),\forall (rho:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),vonNeumann2\left(rho\right)=-\mathrm{re}\left(\mathrm{trace}\left(\mathrm{cfc}\left(((x:\mathbb{R})\mapsto x\cdot \mathrm{Real}.\mathrm{logb}(2,x)),rho\right)\right)\right)$$

Formalization. D5/S3/Divergence/CoherenceL1RelativeEntropyBound.vonNeumann2 (✓ std3).

Citation. Swapan Rana, Preeti Parashar, Maciej Lewenstein (2016). Trace-distance measure of coherence. DOI: 10.1103/PhysRevA.93.012110. URL: https://arxiv.org/abs/1511.01854v2.

Commentary.

Entropy is the negative real trace of x log base two x applied by continuous functional calculus; the scalar function is zero at zero.

Definition 1.3 (The l1 norm of coherence).

$$\forall (n:\mathbb{N}),\forall (rho:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{CorrelatedCoherenceMonogamyRefutation}.l1Coherence(rho)=\sum _{i:\mathrm{Fin}\left(n\right)}(\sum _{j:\mathrm{Fin}\left(n\right)}(\mathrm{if}i\ne j\mathrm{then}\Vert rho(i,j)\Vert \mathrm{else}0))$$

Formalization. D5/S3/Quantum/Information/CorrelatedCoherenceMonogamyRefutation.l1Coherence (✓ std3).

Citation. Swapan Rana, Preeti Parashar, Maciej Lewenstein (2016). Trace-distance measure of coherence. DOI: 10.1103/PhysRevA.93.012110. URL: https://arxiv.org/abs/1511.01854v2.

Commentary.

Section II, Eq. (3b), p. 2 gives Cl1(X) as the sum of |Xij| over i different from j. The complex norm is that absolute value; both indices run through Fin n.

Definition 1.4 (Relative entropy coherence).

$$\forall (n:\mathbb{N}),\forall (rho:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),\mathrm{coherenceRel}\left(rho\right)=vonNeumann2\left(\mathrm{Matrix}.\mathrm{diagonal}(((i:\mathrm{Fin}\left(n\right))\mapsto rho(i,i)))\right)-vonNeumann2\left(rho\right)$$

Formalization. D5/S3/Divergence/CoherenceL1RelativeEntropyBound.coherenceRel (✓ std3).

Citation. Swapan Rana, Preeti Parashar, Maciej Lewenstein (2016). Trace-distance measure of coherence. DOI: 10.1103/PhysRevA.93.012110. URL: https://arxiv.org/abs/1511.01854v2.

Commentary.

Section III, after Eq. (13), p. 4: “The minimization could be solved analytically [2], leading to Cr(ρ) = S(ρdiag)−S(ρ), where S(ρ) = − Tr(ρ log₂ ρ) is the von Neuman entropy.” The scalar functional calculus uses base-two logarithms.

Definition 1.5 (Reflection associated with a matrix).

$$\forall (n:\mathbb{N}),\forall (P:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),\mathrm{reflection}\left(P\right)=2\cdot P-1$$

Formalization. D5/S3/Divergence/CoherenceL1RelativeEntropyBound.reflection (✓ std3).

Source. Repository-derived.

Acknowledgement. Swapan Rana, Preeti Parashar, Maciej Lewenstein (2016). Trace-distance measure of coherence. DOI: 10.1103/PhysRevA.93.012110. URL: https://arxiv.org/abs/1511.01854v2.

Commentary.

The reflection associated with P is twice P minus the identity matrix.

Theorem 1.6 (Hermitian reflections).

$$\forall (n:\mathbb{N}),\forall (P:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),(\mathrm{IsHermitian}\left(P\right))\Rightarrow (\mathrm{IsHermitian}\left(\mathrm{reflection}\left(P\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/Divergence/CoherenceL1RelativeEntropyBound.reflection_hermitian (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Swapan Rana, Preeti Parashar, Maciej Lewenstein (2016). Trace-distance measure of coherence. DOI: 10.1103/PhysRevA.93.012110. URL: https://arxiv.org/abs/1511.01854v2.

Commentary.

The reflection associated with a Hermitian matrix is Hermitian.

Theorem 1.7 (Unitary reflections).

$$\forall (n:\mathbb{N}),\forall (P:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),(\mathrm{IsHermitian}\left(P\right))\Rightarrow ((P\cdot P=P)\Rightarrow (\mathrm{reflection}\left(P\right)\in \mathrm{unitaryGroup}\left(\mathrm{Fin}\left(n\right),\mathbb{C}\right)))$$

Proof. Machine-checked in Lean as D5/S3/Divergence/CoherenceL1RelativeEntropyBound.reflection_unitary (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Swapan Rana, Preeti Parashar, Maciej Lewenstein (2016). Trace-distance measure of coherence. DOI: 10.1103/PhysRevA.93.012110. URL: https://arxiv.org/abs/1511.01854v2.

Commentary.

The reflection associated with a Hermitian idempotent matrix is unitary.

Theorem 1.8 (Hermitian coherence from the upper triangle).

$$\forall (n:\mathbb{N}),\forall (rho:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),(\mathrm{Matrix}.\mathrm{IsHermitian}(rho))\Rightarrow (D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{CorrelatedCoherenceMonogamyRefutation}.l1Coherence(rho)=2\cdot \sum _{k:\mathrm{Fin}\left(n\right)}(\mathrm{norm}\left(\mathrm{WithLp}.\mathrm{toLp}(1,((j:\mathrm{Fin}\left(n\right))\mapsto \mathrm{if}k<j\mathrm{then}rho(k,j)\mathrm{else}0))\right)))$$

Proof. Machine-checked in Lean as D5/S3/Divergence/CoherenceL1RelativeEntropyBound.coherenceL1_eq_twice_upper (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a Hermitian matrix, the l1 coherence equals twice the sum of the l1 norms of the strict upper rows.

Theorem 1.9 (Squared norm as a dot product).

$$\forall (n:\mathbb{N}),\forall (v:\mathrm{Fin}\left(n\right)\to \mathbb{C}),\mathrm{dotProduct}\left(v,\mathrm{star}\left(v\right)\right)=\mathrm{ofReal}\left(\sum _{j:\mathrm{Fin}\left(n\right)}(\mathrm{norm}{\left(v(j)\right)}^2)\right)$$

Proof. Machine-checked in Lean as D5/S3/Divergence/CoherenceL1RelativeEntropyBound.vector_dot_star (✓ std3). ∎

Source. Repository-derived.

Commentary.

The dot product of a complex vector with its entrywise conjugate is the complex embedding of the sum of its squared coordinate norms.

Definition 1.10 (Conjecture 7).

$$claim\iff \forall (n:\mathbb{N}),\forall (rho:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),(\mathrm{IsState}\left(rho\right))\Rightarrow (\mathrm{coherenceRel}\left(rho\right)\le D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{CorrelatedCoherenceMonogamyRefutation}.l1Coherence(rho))$$

Formalization. D5/S3/Divergence/CoherenceL1RelativeEntropyBound.claim (✓ std3).

Citation. Swapan Rana, Preeti Parashar, Maciej Lewenstein (2016). Trace-distance measure of coherence. DOI: 10.1103/PhysRevA.93.012110. URL: https://arxiv.org/abs/1511.01854v2.

Commentary.

Section III.2, printed p. 5, verbatim: “Conjecture 7. For all states ρ, C_{l1}(ρ) ≥ C_r(ρ).” Here n ranges over every natural number and rho over every complex n by n matrix. The state predicate imposes positive semidefiniteness and unit trace, including singular states.

Theorem 1.11 (The coherence inequality).

$$\forall (n:\mathbb{N}),\forall (rho:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),(\mathrm{IsState}\left(rho\right))\Rightarrow (\mathrm{coherenceRel}\left(rho\right)\le D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{CorrelatedCoherenceMonogamyRefutation}.l1Coherence(rho))$$

Proof. Machine-checked in Lean as D5/S3/Divergence/CoherenceL1RelativeEntropyBound.result (✓ std3). ∎

Resolves. Problems/rana-parashar-lewenstein-2016-l1-relative-entropy-coherence (proved) by D5/S3/Divergence/CoherenceL1RelativeEntropyBound.result.

Source. Repository-derived.

Acknowledgement. Swapan Rana, Preeti Parashar, Maciej Lewenstein (2016). Trace-distance measure of coherence. DOI: 10.1103/PhysRevA.93.012110. URL: https://arxiv.org/abs/1511.01854v2.

Commentary.

A binary pinching is the average of a state and its conjugate by the unitary reflection 2P minus the identity. The binary Holevo inequality bounds its entropy increase by twice the trace norm of the off-diagonal block. Sequential coordinate pinchings preserve positivity and trace and end at the diagonal matrix. Each block has one nonzero row, so its trace norm is the square root of the sum of squared absolute values in that row above the diagonal. Summing the entropy increments gives Cᵣ(rho) ≤ 2 sum over k of the upper-row l2 norms. Each row l2 norm is at most its l1 norm, and Hermitian symmetry makes twice the upper-triangular sum equal l1Coherence.

References

• Truth anchor: D5/S3/Divergence/CoherenceL1RelativeEntropyBound.IsState
• Truth anchor: D5/S3/Divergence/CoherenceL1RelativeEntropyBound.claim
• Truth anchor: D5/S3/Divergence/CoherenceL1RelativeEntropyBound.coherenceL1_eq_twice_upper
• Truth anchor: D5/S3/Divergence/CoherenceL1RelativeEntropyBound.coherenceRel
• Truth anchor: D5/S3/Divergence/CoherenceL1RelativeEntropyBound.reflection
• Truth anchor: D5/S3/Divergence/CoherenceL1RelativeEntropyBound.reflection_hermitian
• Truth anchor: D5/S3/Divergence/CoherenceL1RelativeEntropyBound.reflection_unitary
• Truth anchor: D5/S3/Divergence/CoherenceL1RelativeEntropyBound.result
• Truth anchor: D5/S3/Divergence/CoherenceL1RelativeEntropyBound.vector_dot_star
• Truth anchor: D5/S3/Divergence/CoherenceL1RelativeEntropyBound.vonNeumann2
• Truth anchor: D5/S3/Quantum/Information/CorrelatedCoherenceMonogamyRefutation.l1Coherence
• Dependency: D5/S3/Divergence/AudenaertBinaryHolevoBound
• Dependency: D5/S3/Quantum/Dynamics/TridiagonalSweeps/FinitePathDynamics
• Dependency: D5/S3/Quantum/Foundation/FiniteKrausChannel
• Dependency: D5/S3/Quantum/Information/CorrelatedCoherenceMonogamyRefutation