FactorWidthTwoCone

Abstract

Finite support cones and factor-width-two trace duality.

Definition 1.1 (IsKSparse).

$$\forall (n:\mathbb{N}),\forall (k:\mathbb{N}),\forall (v:\mathrm{Fin}n\to \mathbb{C}),\mathrm{IsKSparse}kv=((\mathrm{Finset}.\mathrm{filter}(\mathrm{fun}(i:\mathrm{Fin}n)\mapsto vi\ne 0)\mathrm{Finset}.\mathrm{univ}).\mathrm{card}\le k)$$

Formalization. D5/S3/Quantum/Measurement/FactorWidthTwoCone.IsKSparse (✓ std3).

Citation. Nathaniel Johnston; Shirin Moein; Rajesh Pereira; Sarah Plosker (2022). Absolutely k-incoherent quantum states and spectral inequalities for factor width of a matrix. DOI: 10.1103/PhysRevA.106.052417. URL: https://arxiv.org/abs/2205.05110v2.

Commentary.

Section 2.1, page 3: “In the special case when each vⱼ can be chosen to have at most k non-zero entries (where 1 ≤ k ≤ n), ρ is called k-incoherent”. The finite support counts the nonzero coordinates of v.

Definition 1.2 (IsKIncoherentSum).

$$\forall (n:\mathbb{N}),\forall (k:\mathbb{N}),\forall (X:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),\mathrm{IsKIncoherentSum}kX=(\exists (m:\mathbb{N}),\exists (v:\mathrm{Fin}m\to \mathrm{Fin}n\to \mathbb{C}),(\forall (j:\mathrm{Fin}m),\mathrm{IsKSparse}k(vj))\wedge (X=\sum _{(j:\mathrm{Fin}m)}\mathrm{Matrix}.\mathrm{vecMulVec}(vj)(\mathrm{star}(vj))))$$

Formalization. D5/S3/Quantum/Measurement/FactorWidthTwoCone.IsKIncoherentSum (✓ std3).

Citation. Nathaniel Johnston; Shirin Moein; Rajesh Pereira; Sarah Plosker (2022). Absolutely k-incoherent quantum states and spectral inequalities for factor width of a matrix. DOI: 10.1103/PhysRevA.106.052417. URL: https://arxiv.org/abs/2205.05110v2.

Commentary.

Section 2.1, page 3: “every mixed state ρ ∈ Mₙ⁺ can be written in the form ρ = Σⱼ vⱼvⱼ* for some {vⱼ} ⊆ ℂⁿ. In the special case when each vⱼ can be chosen to have at most k non-zero entries (where 1 ≤ k ≤ n), ρ is called k-incoherent”. Here j ranges over Fin m, and no normalization is imposed on the individual vectors.

Definition 1.3 (IsLocally2).

$$\forall (n:\mathbb{N}),\forall (Y:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),IsLocally2(Y)=(((Y).\mathrm{IsHermitian})\wedge (\forall (s:\mathrm{Subtype}(\mathrm{fun}(s:\mathrm{Finset}(\mathrm{Fin}n))\mapsto (s).\mathrm{card}\le 2)),\forall (x:\mathrm{Fin}n\to \mathbb{C}),(\forall (j:\mathrm{Fin}n),(\neg (j\in (s).\mathrm{val}))\to xj=0)\to 0\le \mathrm{RHLinalg}.\mathrm{hermForm}Yx))$$

Formalization. D5/S3/Quantum/Measurement/FactorWidthTwoCone.IsLocally2 (✓ std3).

Citation. Nathaniel Johnston; Shirin Moein; Rajesh Pereira; Sarah Plosker (2022). Absolutely k-incoherent quantum states and spectral inequalities for factor width of a matrix. DOI: 10.1103/PhysRevA.106.052417. URL: https://arxiv.org/abs/2205.05110v2.

Commentary.

Definition 1(b), page 4: “⟨v|X|v⟩ ≥ 0 for all |v⟩ ∈ ℂⁿ with at most k non-zero entries; or”. Here k = 2; s ranges over coordinate subsets with cardinality at most two, and x vanishes outside s.

Theorem 1.4 (fw2 duality).

$$\forall (n:\mathbb{N}),\forall (X:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),((X).\mathrm{IsHermitian})\to (\forall (A:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),(IsLocally2(A))\to 0\le \mathrm{RHLinalg}.\mathrm{rtrace}(X\cdot A))\to \mathrm{IsKIncoherentSum}2X$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/FactorWidthTwoCone.fw2_duality (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Nathaniel Johnston; Shirin Moein; Rajesh Pereira; Sarah Plosker (2022). Absolutely k-incoherent quantum states and spectral inequalities for factor width of a matrix. DOI: 10.1103/PhysRevA.106.052417. URL: https://arxiv.org/abs/2205.05110v2.

Commentary.

Nonnegative trace pairing against all locally positive matrices implies a finite sum of outer products of two-sparse vectors. Closedness of the finite family of support cones gives the separating Hermitian matrix.

Theorem 1.5 (local2 diagonal).

$$\forall (n:\mathbb{N}),\forall (A:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),(IsLocally2(A))\to \forall (i:\mathrm{Fin}n),0\le (Aii).\mathrm{re}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/FactorWidthTwoCone.local2_diagonal (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Nathaniel Johnston; Shirin Moein; Rajesh Pereira; Sarah Plosker (2022). Absolutely k-incoherent quantum states and spectral inequalities for factor width of a matrix. DOI: 10.1103/PhysRevA.106.052417. URL: https://arxiv.org/abs/2205.05110v2.

Commentary.

Every diagonal entry of a locally positive matrix is nonnegative.

Theorem 1.6 (local2 minor).

$$\forall (n:\mathbb{N}),\forall (A:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),(IsLocally2(A))\to \forall (i:\mathrm{Fin}n),\forall (j:\mathrm{Fin}n),\mathrm{Complex}.\mathrm{normSq}(Aij)\le (Aii).\mathrm{re}\cdot (Ajj).\mathrm{re}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/FactorWidthTwoCone.local2_minor (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Nathaniel Johnston; Shirin Moein; Rajesh Pereira; Sarah Plosker (2022). Absolutely k-incoherent quantum states and spectral inequalities for factor width of a matrix. DOI: 10.1103/PhysRevA.106.052417. URL: https://arxiv.org/abs/2205.05110v2.

Commentary.

Each two-coordinate principal submatrix is positive semidefinite, so its determinant bounds its off-diagonal entry.

Theorem 1.7 (local2 smul).

$$\forall (n:\mathbb{N}),\forall (A:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),(IsLocally2(A))\to \forall (c:\mathbb{R}),(0\le c)\to IsLocally2(\mathrm{HSMul}.\mathrm{hSMul}cA)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/FactorWidthTwoCone.local2_smul (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Nathaniel Johnston; Shirin Moein; Rajesh Pereira; Sarah Plosker (2022). Absolutely k-incoherent quantum states and spectral inequalities for factor width of a matrix. DOI: 10.1103/PhysRevA.106.052417. URL: https://arxiv.org/abs/2205.05110v2.

Commentary.

Multiplication by a nonnegative real scalar preserves local positivity.

Theorem 1.8 (local2 trace nonneg).

$$\forall (n:\mathbb{N}),\forall (A:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),(IsLocally2(A))\to 0\le \mathrm{RHLinalg}.\mathrm{rtrace}(A)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/FactorWidthTwoCone.local2_trace_nonneg (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Nathaniel Johnston; Shirin Moein; Rajesh Pereira; Sarah Plosker (2022). Absolutely k-incoherent quantum states and spectral inequalities for factor width of a matrix. DOI: 10.1103/PhysRevA.106.052417. URL: https://arxiv.org/abs/2205.05110v2.

Commentary.

The real trace of a locally positive matrix is nonnegative.

Theorem 1.9 (local2 trace zero).

$$\forall (n:\mathbb{N}),\forall (A:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),(IsLocally2(A))\to (\mathrm{RHLinalg}.\mathrm{rtrace}(A)=0)\to A=0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/FactorWidthTwoCone.local2_trace_zero (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Nathaniel Johnston; Shirin Moein; Rajesh Pereira; Sarah Plosker (2022). Absolutely k-incoherent quantum states and spectral inequalities for factor width of a matrix. DOI: 10.1103/PhysRevA.106.052417. URL: https://arxiv.org/abs/2205.05110v2.

Commentary.

A locally positive matrix with zero real trace vanishes.

References

• Truth anchor: D5/S3/Quantum/Measurement/FactorWidthTwoCone.IsKIncoherentSum
• Truth anchor: D5/S3/Quantum/Measurement/FactorWidthTwoCone.IsKSparse
• Truth anchor: D5/S3/Quantum/Measurement/FactorWidthTwoCone.IsLocally2
• Truth anchor: D5/S3/Quantum/Measurement/FactorWidthTwoCone.fw2_duality
• Truth anchor: D5/S3/Quantum/Measurement/FactorWidthTwoCone.local2_diagonal
• Truth anchor: D5/S3/Quantum/Measurement/FactorWidthTwoCone.local2_minor
• Truth anchor: D5/S3/Quantum/Measurement/FactorWidthTwoCone.local2_smul
• Truth anchor: D5/S3/Quantum/Measurement/FactorWidthTwoCone.local2_trace_nonneg
• Truth anchor: D5/S3/Quantum/Measurement/FactorWidthTwoCone.local2_trace_zero
• Dependency: D5/S3/Quantum/Matrix/CartesianVariance
• Dependency: D5/S3/Quantum/Measurement/IncoherentCone