QubitWassersteinCouplings

Abstract

Qubit coupling optimization and the exact Pauli self cost.

Definition 1.1 (couplings).

$$\forall d\in \mathbb{N},\forall rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall omega\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\mathrm{couplings}\left(rho,omega\right)=\{pi:\mathrm{Matrix}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right)\right),\mathrm{Prod}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right)\right),\mathbb{C}\right)|((\mathrm{Matrix}.\mathrm{PosSemidef}\left(pi\right))\wedge (\mathrm{Matrix}.\mathrm{trace}\left(pi\right)=1))\wedge ((\mathrm{PartialTraceMutualInformation}.\mathrm{partialTraceRight}\left(pi\right)=omega)\wedge (\mathrm{PartialTraceMutualInformation}.\mathrm{partialTraceLeft}\left(pi\right)=\mathrm{Matrix}.\mathrm{transpose}\left(rho\right)))\}$$

Formalization. D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.couplings (✓ std3).

Citation. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

The source §1.2 coupling set consists of positive semidefinite trace-one matrices on the product index type, with second-factor trace omega and first-factor trace rho transpose. The partialTraceRight and partialTraceLeft are literally the explicit sums over the traced-out factor.

Definition 1.2 (cost).

$$\forall d\in \mathbb{N},\forall k\in \mathbb{N},\forall A\in \mathrm{Fin}\left(k\right)\to \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall pi\in \mathrm{Matrix}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right)\right),\mathrm{Prod}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right)\right),\mathbb{C}\right),\mathrm{cost}\left(A,pi\right)=\sum _{j:\mathrm{Fin}\left(k\right)}(\mathrm{RCLike}.\mathrm{re}\left(\mathrm{Matrix}.\mathrm{trace}\left(((\mathrm{Matrix}.\mathrm{kronecker}\left(A\left(j\right),1\right)-\mathrm{Matrix}.\mathrm{kronecker}\left(1,\mathrm{Matrix}.\mathrm{transpose}\left(A\left(j\right)\right)\right))\cdot (pi))\cdot (\mathrm{Matrix}.\mathrm{kronecker}\left(A\left(j\right),1\right)-\mathrm{Matrix}.\mathrm{kronecker}\left(1,\mathrm{Matrix}.\mathrm{transpose}\left(A\left(j\right)\right)\right))\right)\right))$$

Formalization. D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.cost (✓ std3).

Citation. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

The trace cost is equation (eq:2-Wass-quant-def), with transpose on the dual factor and its real part made explicit.

Definition 1.3 (D2).

$$\forall d\in \mathbb{N},\forall k\in \mathbb{N},\forall A\in \mathrm{Fin}\left(k\right)\to \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall omega\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),D2\left(A,rho,omega\right)=\mathrm{sInf}\left(\mathrm{Set}.\mathrm{image}\left(\mathrm{cost}\left(A\right),\mathrm{couplings}\left(rho,omega\right)\right)\right)$$

Formalization. D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.D2 (✓ std3).

Citation. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

The quadratic quantum Wasserstein distance is the infimum in equation (eq:2-Wass-quant-def).

Definition 1.4 (dA).

$$\forall d\in \mathbb{N},\forall k\in \mathbb{N},\forall A\in \mathrm{Fin}\left(k\right)\to \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall omega\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\mathrm{dA}\left(A,rho,omega\right)=\mathrm{Real}.\mathrm{sqrt}\left(D2\left(A,rho,omega\right)-\frac{D2\left(A,rho,rho\right)+D2\left(A,omega,omega\right)}{2}\right)$$

Formalization. D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.dA (✓ std3).

Citation. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

The divergence is equation (eq:mod-qw-dist-def); the displayed fraction is real division.

Definition 1.5 (CW).

$$\forall d\in \mathbb{N},\forall k\in \mathbb{N},\forall A\in \mathrm{Fin}\left(k\right)\to \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall Phi\in \mathrm{LinearMap}\left(\mathbb{C},\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)\right),\mathrm{CW}\left(A,Phi\right)=\mathrm{sSup}\left(\{x:\mathbb{R}|\exists rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),(\mathrm{CoPRelativeQuantumnessRefutation}.\mathrm{IsDensity}\left(rho\right))\wedge (x=\mathrm{dA}\left(A,rho,Phi\left(rho\right)\right))\}\right)$$

Formalization. D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.CW (✓ std3).

Citation. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

Source §5.1, PDF p. 17, verbatim: “Given a finite collections of observables 𝒜={A₁, …, Aₖ}, let us define the Wasserstein complexity of a channel Φ:𝒮(ℋ)→𝒮(ℋ) by C_W(Φ):=max_{ρ∈𝒮(ℋ)} d_𝒜(ρ, Φ(ρ)).” The finite-dimensional source maximum is encoded by the supremum of its values; CW_bddAbove supplies boundedness.

Theorem 1.6 (product_coupling).

$$\forall d\in \mathbb{N},\forall rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall omega\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),(\mathrm{CoPRelativeQuantumnessRefutation}.\mathrm{IsDensity}\left(rho\right))\Rightarrow ((\mathrm{CoPRelativeQuantumnessRefutation}.\mathrm{IsDensity}\left(omega\right))\Rightarrow (\mathrm{Matrix}.\mathrm{kronecker}\left(omega,\mathrm{Matrix}.\mathrm{transpose}\left(rho\right)\right)\in \mathrm{couplings}\left(rho,omega\right)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.product_coupling (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

The product of the output state and the transposed input state is an admissible coupling.

Theorem 1.7 (couplings_nonempty).

$$\forall d\in \mathbb{N},\forall rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall omega\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),(\mathrm{CoPRelativeQuantumnessRefutation}.\mathrm{IsDensity}\left(rho\right))\Rightarrow ((\mathrm{CoPRelativeQuantumnessRefutation}.\mathrm{IsDensity}\left(omega\right))\Rightarrow (\mathrm{Set}.\mathrm{Nonempty}\left(\mathrm{couplings}\left(rho,omega\right)\right)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.couplings_nonempty (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

Every pair of density states has a coupling.

Theorem 1.8 (D2_le_cost).

$$\forall d\in \mathbb{N},\forall k\in \mathbb{N},\forall A\in \mathrm{Fin}\left(k\right)\to \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall omega\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall pi\in \mathrm{Matrix}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right)\right),\mathrm{Prod}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right)\right),\mathbb{C}\right),(\forall j\in \mathrm{Fin}\left(k\right),\mathrm{Matrix}.\mathrm{IsHermitian}\left(A\left(j\right)\right))\Rightarrow ((pi\in \mathrm{couplings}\left(rho,omega\right))\Rightarrow (D2\left(A,rho,omega\right)\le \mathrm{cost}\left(A,pi\right)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.D2_le_cost (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

Every admissible coupling bounds the infimum from above.

Theorem 1.9 (pauli_hermitian).

$$\forall j\in \mathrm{Fin}\left(3\right),\mathrm{Matrix}.\mathrm{IsHermitian}\left(\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{pauli}\left(j\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.pauli_hermitian (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

Every observable in the Pauli triple is Hermitian.

Theorem 1.10 (ptrace2_left).

$$\forall U\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),\forall P\in \mathrm{Matrix}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right)\right),\mathrm{Prod}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right)\right),\mathbb{C}\right),\mathrm{PartialTraceMutualInformation}.\mathrm{partialTraceRight}\left(((\mathrm{Matrix}.\mathrm{kronecker}\left(U,1\right))\cdot (P))\cdot (\mathrm{Matrix}.\mathrm{conjTranspose}\left(\mathrm{Matrix}.\mathrm{kronecker}\left(U,1\right)\right))\right)=((U)\cdot (\mathrm{PartialTraceMutualInformation}.\mathrm{partialTraceRight}\left(P\right)))\cdot (\mathrm{Matrix}.\mathrm{conjTranspose}\left(U\right))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.ptrace2_left (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

Conjugating a two-qubit operator by a local matrix on the first factor conjugates its second-factor partial trace by that matrix.

Definition 1.11 (overlap).

$$\forall P\in \mathrm{Matrix}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right)\right),\mathrm{Prod}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right)\right),\mathbb{C}\right),\mathrm{overlap}\left(P\right)=\mathrm{Complex}.\mathrm{re}\left(\mathrm{dotProduct}\left(\mathrm{star}\left(\mathrm{Function}.\mathrm{uncurry}\left((1:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right))\right)\right),\mathrm{Matrix}.\mathrm{mulVec}\left(P,\mathrm{Function}.\mathrm{uncurry}\left((1:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right))\right)\right)\right)\right)$$

Formalization. D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.overlap (✓ std3).

Source. Repository-derived.

Acknowledgement. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

The unnormalized Bell overlap is the quadratic form of P on Function.uncurry of the identity matrix.

Theorem 1.12 (pauli_cost).

$$\forall P\in \mathrm{Matrix}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right)\right),\mathrm{Prod}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right)\right),\mathbb{C}\right),\mathrm{cost}\left(\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{pauli},P\right)=(8)\cdot (\mathrm{Complex}.\mathrm{re}\left(\mathrm{Matrix}.\mathrm{trace}\left(P\right)\right))-(4)\cdot (\mathrm{overlap}\left(P\right))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.pauli_cost (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

The Pauli cost operator is 8 times the identity minus 4 times the unnormalized Bell rank-one operator, equivalently 8 times the difference of the identity and the normalized Bell projector.

Theorem 1.13 (CW_bddAbove).

$$\forall d\in \mathbb{N},\forall k\in \mathbb{N},\forall A\in \mathrm{Fin}\left(k\right)\to \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall Phi\in \mathrm{LinearMap}\left(\mathbb{C},\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)\right),(\forall j\in \mathrm{Fin}\left(k\right),\mathrm{Matrix}.\mathrm{IsHermitian}\left(A\left(j\right)\right))\Rightarrow (\mathrm{BddAbove}\left(\{x:\mathbb{R}|\exists rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),(\mathrm{CoPRelativeQuantumnessRefutation}.\mathrm{IsDensity}\left(rho\right))\wedge (x=\mathrm{dA}\left(A,rho,Phi\left(rho\right)\right))\}\right))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.CW_bddAbove (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

The complexity value set is bounded above, including the empty zero-dimensional domain.

Definition 1.14 (pureCoupling).

$$\forall d\in \mathbb{N},\forall S\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\mathrm{pureCoupling}\left(S\right)=\mathrm{PureStateHandshake}.\mathrm{rankOneDensity}\left(\mathrm{Function}.\mathrm{uncurry}\left(S\right)\right)$$

Formalization. D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.pureCoupling (✓ std3).

Source. Repository-derived.

Acknowledgement. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

The square-root coupling reuses the frozen rank-one density construction on the vectorized matrix.

Theorem 1.15 (pureCoupling_psd).

$$\forall d\in \mathbb{N},\forall S\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\mathrm{Matrix}.\mathrm{PosSemidef}\left(\mathrm{pureCoupling}\left(S\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.pureCoupling_psd (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

A vectorized outer product is positive semidefinite.

Theorem 1.16 (ptrace2_pure).

$$\forall d\in \mathbb{N},\forall S\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\mathrm{PartialTraceMutualInformation}.\mathrm{partialTraceRight}\left(\mathrm{pureCoupling}\left(S\right)\right)=(S)\cdot (\mathrm{Matrix}.\mathrm{conjTranspose}\left(S\right))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.ptrace2_pure (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

The second-factor trace of the vectorized coupling is S times S conjugate transpose.

Theorem 1.17 (ptrace1_pure).

$$\forall d\in \mathbb{N},\forall S\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\mathrm{PartialTraceMutualInformation}.\mathrm{partialTraceLeft}\left(\mathrm{pureCoupling}\left(S\right)\right)=\mathrm{Matrix}.\mathrm{transpose}\left((\mathrm{Matrix}.\mathrm{conjTranspose}\left(S\right))\cdot (S)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.ptrace1_pure (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

The first-factor trace is the transpose of S conjugate transpose times S.

Theorem 1.18 (overlap_pure).

$$\forall S\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),\mathrm{overlap}\left(\mathrm{pureCoupling}\left(S\right)\right)=\mathrm{Complex}.\mathrm{normSq}\left(\mathrm{Matrix}.\mathrm{trace}\left(S\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.overlap_pure (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

The Bell overlap of the vectorized coupling is the squared complex norm of its trace.

Theorem 1.19 (diagState_isState).

$$\forall a\in \mathbb{R},\forall b\in \mathbb{R},(0\le a)\Rightarrow ((0\le b)\Rightarrow ((a+b=1)\Rightarrow (\mathrm{CoPRelativeQuantumnessRefutation}.\mathrm{IsDensity}\left(\mathrm{ProjectedUnistochasticDynamics}.\mathrm{diagonalState}\left(![a,b]\right)\right))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.diagState_isState (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

Nonnegative diagonal entries summing to one give a density state.

Theorem 1.20 (diag_self_cost).

$$\forall a\in \mathbb{R},\forall b\in \mathbb{R},(0\le a)\Rightarrow ((0\le b)\Rightarrow ((a+b=1)\Rightarrow (D2\left(\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{pauli},\mathrm{ProjectedUnistochasticDynamics}.\mathrm{diagonalState}\left(![a,b]\right),\mathrm{ProjectedUnistochasticDynamics}.\mathrm{diagonalState}\left(![a,b]\right)\right)=8-(4)\cdot ((\mathrm{Real}.\mathrm{sqrt}\left(a\right)+\mathrm{Real}.\mathrm{sqrt}\left(b\right){)}^2))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.diag_self_cost (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

The diagonal optimum is attained by the vectorized square root; the principal-minor bound gives the matching lower bound.

Theorem 1.21 (rotate_isState).

$$\forall U\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),\mathrm{Fin}\left(2\right),\mathbb{C}\right),((\mathrm{Matrix}.\mathrm{conjTranspose}\left(U\right))\cdot (U)=1)\Rightarrow ((\mathrm{CoPRelativeQuantumnessRefutation}.\mathrm{IsDensity}\left(rho\right))\Rightarrow (\mathrm{CoPRelativeQuantumnessRefutation}.\mathrm{IsDensity}\left(\mathrm{ProjectedUnistochasticDynamics}.\mathrm{unitaryEvolution}\left(U,rho\right)\right)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.rotate_isState (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

Unitary conjugation preserves density states.

Theorem 1.22 (D2_rotate).

$$\forall U\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),\mathrm{Fin}\left(2\right),\mathbb{C}\right),\forall omega\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),((\mathrm{Matrix}.\mathrm{conjTranspose}\left(U\right))\cdot (U)=1)\Rightarrow (((U)\cdot (\mathrm{Matrix}.\mathrm{conjTranspose}\left(U\right))=1)\Rightarrow ((\mathrm{CoPRelativeQuantumnessRefutation}.\mathrm{IsDensity}\left(rho\right))\Rightarrow ((\mathrm{CoPRelativeQuantumnessRefutation}.\mathrm{IsDensity}\left(omega\right))\Rightarrow (D2\left(\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{pauli},\mathrm{ProjectedUnistochasticDynamics}.\mathrm{unitaryEvolution}\left(U,rho\right),\mathrm{ProjectedUnistochasticDynamics}.\mathrm{unitaryEvolution}\left(U,omega\right)\right)=D2\left(\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{pauli},rho,omega\right)))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.D2_rotate (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

The Pauli infimum is invariant under simultaneous unitary conjugation, by transporting couplings through U tensor conjugate U.

Theorem 1.23 (self_cost_spectral).

$$\forall rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),(\mathrm{CoPRelativeQuantumnessRefutation}.\mathrm{IsDensity}\left(rho\right))\Rightarrow (\exists a\in \mathbb{R},\exists b\in \mathbb{R},(0\le a)\wedge ((0\le b)\wedge ((a+b=1)\wedge ((D2\left(\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{pauli},rho,rho\right)=8-(4)\cdot ((\mathrm{Real}.\mathrm{sqrt}\left(a\right)+\mathrm{Real}.\mathrm{sqrt}\left(b\right){)}^2))\wedge (\mathrm{Complex}.\mathrm{re}\left(\mathrm{Matrix}.\mathrm{trace}\left(\mathrm{CFC}.\mathrm{sqrt}\left(rho\right)\right)\right)=\mathrm{Real}.\mathrm{sqrt}\left(a\right)+\mathrm{Real}.\mathrm{sqrt}\left(b\right))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.self_cost_spectral (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

Spectral reduction supplies nonnegative eigenvalues summing to one, the exact self cost and the real trace of the positive square root.

Theorem 1.24 (self_cost).

$$\forall rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),(\mathrm{CoPRelativeQuantumnessRefutation}.\mathrm{IsDensity}\left(rho\right))\Rightarrow (D2\left(\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{pauli},rho,rho\right)=8-(4)\cdot ((\mathrm{Complex}.\mathrm{re}\left(\mathrm{Matrix}.\mathrm{trace}\left(\mathrm{CFC}.\mathrm{sqrt}\left(rho\right)\right)\right){)}^2))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.self_cost (✓ std3). ∎

Citation. G. Bunth; J. Pitrik; T. Titkos; D. Virosztek (2024). On the metric property of quantum Wasserstein divergences. DOI: 10.1103/PhysRevA.110.022211. URL: https://arxiv.org/abs/2402.13150v4.

Commentary.

Section 4.1, Proposition 3, equation (35), states D²(ρ,ρ)=4(1−√(1−|bρ|²)); for eigenvalues (1±r)/2 this is 8−4(tr√ρ)², the displayed correspondence.

References

• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.CW
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.CW_bddAbove
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.D2
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.D2_le_cost
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.D2_rotate
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.cost
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.couplings
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.couplings_nonempty
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.dA
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.diagState_isState
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.diag_self_cost
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.overlap
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.overlap_pure
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.pauli_cost
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.pauli_hermitian
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.product_coupling
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.ptrace1_pure
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.ptrace2_left
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.ptrace2_pure
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.pureCoupling
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.pureCoupling_psd
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.rotate_isState
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.self_cost
• Truth anchor: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings.self_cost_spectral
• Dependency: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction
• Dependency: D5/S3/Quantum/Matrix/CartesianVariance
• Dependency: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation
• Dependency: D5/S3/Quantum/PureState/PureStateHandshake
• Dependency: D5/S3/QuantumChannels/CoPRelativeQuantumnessRefutation