The three-state root-fidelity Holevo bound

Abstract

Root-fidelity matrix entropy bounds the Holevo quantity of every three-state ensemble.

Definition 1.1 (Holevo quantity).

$$\forall n\in \mathrm{Type},[\mathrm{Fintype}\left(n\right)][\mathrm{DecidableEq}\left(n\right)]\forall p\in \mathrm{Fin}\left(3\right)\to \mathbb{R},\forall rho\in \mathrm{Fin}\left(3\right)\to \mathrm{Matrix}\left(n,n,\mathbb{C}\right),\mathrm{holevo}\left(p,rho\right)=-(Complex.re\left(Matrix.trace\left((\sum _{i:\mathrm{Fin}\left(3\right)}((p\left(i\right):\mathbb{C})\cdot rho\left(i\right)))\cdot CFC.log\left(\sum _{i:\mathrm{Fin}\left(3\right)}((p\left(i\right):\mathbb{C})\cdot rho\left(i\right))\right)\right)\right))-\sum _{i:\mathrm{Fin}\left(3\right)}(p\left(i\right)\cdot -(Complex.re\left(Matrix.trace\left((rho\left(i\right))\cdot CFC.log\left(rho\left(i\right)\right)\right)\right)))$$

Formalization. D5/S3/Quantum/Divergence/FannesRootFidelityHolevo.holevo (✓ std3).

Citation. M. Fannes, F. de Melo, W. Roga, K. Życzkowski (2011). Matrices of fidelities for ensembles of quantum states and the Holevo quantity. URL: https://arxiv.org/abs/1104.2271v1.

Commentary.

Equation (2), page 3: χ(Eₖ) = S(ϱ) − ∑ᵢ pᵢ S(ϱᵢ), where ϱ = ∑ᵢ pᵢϱᵢ. Here the ensemble index is Fin 3.

Definition 1.2 (Root-fidelity matrix).

$$\forall n\in \mathrm{Type},[\mathrm{Fintype}\left(n\right)][\mathrm{DecidableEq}\left(n\right)]\forall p\in \mathrm{Fin}\left(3\right)\to \mathbb{R},\forall rho\in \mathrm{Fin}\left(3\right)\to \mathrm{Matrix}\left(n,n,\mathbb{C}\right),\forall i\in \mathrm{Fin}\left(3\right),\forall j\in \mathrm{Fin}\left(3\right),\mathrm{rootFidelityMatrix}\left(p,rho\right)\left(i,j\right)=((Real.sqrt\left(p\left(i\right)\cdot p\left(j\right)\right)\cdot FiniteTraceDistance.traceNorm\left(CFC.sqrt\left(rho\left(i\right)\right)\cdot CFC.sqrt\left(rho\left(j\right)\right)\right):\mathbb{R}):\mathbb{C})$$

Formalization. D5/S3/Quantum/Divergence/FannesRootFidelityHolevo.rootFidelityMatrix (✓ std3).

Citation. M. Fannes, F. de Melo, W. Roga, K. Życzkowski (2011). Matrices of fidelities for ensembles of quantum states and the Holevo quantity. URL: https://arxiv.org/abs/1104.2271v1.

Commentary.

Equation (16), page 10: C√F(E₃) = [√(pᵢpⱼ)√Fᵢⱼ]ᵢⱼ. Each real matrix entry is embedded in the complex numbers.

Definition 1.3 (Conjecture 1).

$$claim\iff (\forall d\in \mathbb{N},\forall rho\in \mathrm{Fin}\left(3\right)\to \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall p\in \mathrm{Fin}\left(3\right)\to \mathbb{R},(\forall i\in \mathrm{Fin}\left(3\right),(Matrix.PosSemidef\left(rho\left(i\right)\right))\wedge (Matrix.trace\left(rho\left(i\right)\right)=1))\Rightarrow ((\forall i\in \mathrm{Fin}\left(3\right),0\le p\left(i\right))\Rightarrow ((\sum _{i:\mathrm{Fin}\left(3\right)}(p\left(i\right))=1)\Rightarrow (\mathrm{holevo}\left(p,rho\right)\le -(Complex.re\left(Matrix.trace\left((\mathrm{rootFidelityMatrix}\left(p,rho\right))\cdot CFC.log\left(\mathrm{rootFidelityMatrix}\left(p,rho\right)\right)\right)\right))))))$$

Formalization. D5/S3/Quantum/Divergence/FannesRootFidelityHolevo.claim (✓ std3).

Citation. M. Fannes, F. de Melo, W. Roga, K. Życzkowski (2011). Matrices of fidelities for ensembles of quantum states and the Holevo quantity. URL: https://arxiv.org/abs/1104.2271v1.

Commentary.

Page 10, Conjecture 1: For any ensemble E₃ = {(pᵢ, ϱᵢ)} with K = 3 three states of arbitrary dimension d the corresponding Holevo quantity χ(E₃) is bounded from above by the entropy of the matrix C√F(E₃) defined in (16): χ(E₃) ≤ S(C√F(E₃)). A state is a positive semidefinite Matrix (Fin d) (Fin d) ℂ of trace one. The weights are nonnegative and sum to one. Every natural dimension is quantified; dimension zero has no such density matrix.

Theorem 1.4 (The Holevo bound for three arbitrary states).

$$\forall d\in \mathbb{N},\forall rho\in \mathrm{Fin}\left(3\right)\to \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall p\in \mathrm{Fin}\left(3\right)\to \mathbb{R},(\forall i\in \mathrm{Fin}\left(3\right),(Matrix.PosSemidef\left(rho\left(i\right)\right))\wedge (Matrix.trace\left(rho\left(i\right)\right)=1))\Rightarrow ((\forall i\in \mathrm{Fin}\left(3\right),0\le p\left(i\right))\Rightarrow ((\sum _{i:\mathrm{Fin}\left(3\right)}(p\left(i\right))=1)\Rightarrow (\mathrm{holevo}\left(p,rho\right)\le -(Complex.re\left(Matrix.trace\left((\mathrm{rootFidelityMatrix}\left(p,rho\right))\cdot CFC.log\left(\mathrm{rootFidelityMatrix}\left(p,rho\right)\right)\right)\right)))))$$

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

Resolves. Problems/fannes-demelo-roga-zyczkowski-2012-root-fidelity-holevo-bound (proved) by D5/S3/Quantum/Divergence/FannesRootFidelityHolevo.result.

Source. Repository-derived.

Acknowledgement. M. Fannes, F. de Melo, W. Roga, K. Życzkowski (2011). Matrices of fidelities for ensembles of quantum states and the Holevo quantity. URL: https://arxiv.org/abs/1104.2271v1.

Commentary.

Two polar gauges make two cross products positive. An eigenbasis of the remaining polar unitary preserves all three root fidelities in one rank-one decomposition. Channel data processing bounds the Holevo quantity by its labelled rank-one refinement. The three-by-three entrywise-modulus entropy inequality and diagonal entropy accounting then bound that refinement by the entropy of the root-fidelity matrix. Singular states and zero weights require no limiting restriction.

References

• Truth anchor: D5/S3/Quantum/Divergence/FannesRootFidelityHolevo.claim
• Truth anchor: D5/S3/Quantum/Divergence/FannesRootFidelityHolevo.holevo
• Truth anchor: D5/S3/Quantum/Divergence/FannesRootFidelityHolevo.result
• Truth anchor: D5/S3/Quantum/Divergence/FannesRootFidelityHolevo.rootFidelityMatrix
• Dependency: D5/S3/Quantum/Divergence/CanonicalChannelDPI
• Dependency: D5/S3/Quantum/Divergence/CanonicalRelativeModularModel
• Dependency: D5/S3/Quantum/Divergence/SupportAwareRelativeEntropy
• Dependency: D5/S3/Quantum/Divergence/ThreeByThreeModulusEntropy
• Dependency: D5/S3/Quantum/Dynamics/EntropyProductionCoherenceDeletionIdentity
• Dependency: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction
• Dependency: D5/S3/Quantum/Entanglement/UniversalReplacementCapacityGrowth
• Dependency: D5/S3/Quantum/FixedAlgebra/RecordFixedAlgebraDecomposition
• Dependency: D5/S3/Quantum/Foundation/FiniteKrausChannel
• Dependency: D5/S3/Quantum/Foundation/FiniteStateChannel
• Dependency: D5/S3/Quantum/Foundation/FiniteTraceDistance
• Dependency: D5/S3/Quantum/Information/ChenKatoBrandaoCMIRefutation
• Dependency: D5/S3/Quantum/Information/NMLWMeasuredFidelitySeparation
• Dependency: D5/S3/Quantum/Information/PartialTraceMutualInformation
• Dependency: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral
• Dependency: D5/S3/Quantum/Recovery/PurifiedLocalPath
• Dependency: D5/S3/Quantum/Schatten/TraceNorm
• Dependency: D5/S3/Quantum/Schatten/UnitarilyInvariantNorm
• Dependency: D5/S3/QuantumBounds/PeritoTensorBlockBound