Cartesian variance

Abstract

A pure vector maximizes the Cartesian matrix variance.

Theorem 1.1 (Density matrices exist in positive dimension).

$$\forall n\in \mathbb{N},0<n\Rightarrow \left(\exists rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),Matrix.PosSemidef(rho)\wedge Matrix.trace(rho)=1\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/CartesianVariance.density_nonempty (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every positive finite dimension has a positive semidefinite matrix of trace one.

Theorem 1.2 (Positive semidefinite entry bound).

$$\forall n\in Type,[\mathrm{Fintype}\left(n\right)][\mathrm{DecidableEq}\left(n\right)],\forall P\in \mathrm{Matrix}\left(n,n,\mathbb{C}\right),i\in n,j\in n,Matrix.PosSemidef(P)\Rightarrow Complex.normSq(P(i,j))\le Complex.re(P(i,i))\cdot Complex.re(P(j,j))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/CartesianVariance.psd_entry_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

A two-by-two principal minor bounds each squared entry modulus by the product of its diagonal entries. The estimate bounds the entries of density matrices and controls positive semidefinite summands in the incoherent cone.

Theorem 1.3 (Spectral expansion into rank-one matrices).

$$\forall n\in \mathbb{N},rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),h\in Matrix.IsHermitian(rho),rho=\sum _{i:\mathrm{Fin}\left(n\right)}(\mathrm{eigenvalues}\left(h,i\right)\cdot (Matrix.vecMulVec(WithLp.ofLp(\mathrm{eigenvectorBasis}\left(h,i\right)),\mathrm{star}\left(WithLp.ofLp(\mathrm{eigenvectorBasis}\left(h,i\right))\right))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/CartesianVariance.hermitian_spectral_sum (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every finite Hermitian complex matrix is the sum of its eigenvalues times the rank-one projections onto its orthonormal eigenvectors.

Theorem 1.4 (A density spectrum sums to one).

$$\forall n\in \mathbb{N},rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),h\in \left(Matrix.PosSemidef(rho)\wedge Matrix.trace(rho)=1\right),\sum _{i:\mathrm{Fin}\left(n\right)}(Matrix.IsHermitian.eigenvalues(Matrix.PosSemidef.isHermitian(h.1),i))=1$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/CartesianVariance.density_eigenvalues_sum (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a positive semidefinite trace-one complex matrix, the real eigenvalues sum to one. The Hermitian proof is the first component of h followed by Matrix.PosSemidef.isHermitian.

Theorem 1.5 (Frobenius square in coordinates).

$$\forall n\in \mathbb{N},A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),RHLinalg.frobSq(A)=\sum _{i:\mathrm{Fin}\left(n\right)}(\sum _{j:\mathrm{Fin}\left(n\right)}(Complex.normSq(A(j,i))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/CartesianVariance.frobSq_eq_sum (✓ std3). ∎

Source. Repository-derived.

Commentary.

The squared Frobenius norm is the sum of the squared moduli of all matrix entries.

Theorem 1.6 (Nonnegative Frobenius square).

$$\forall n\in \mathbb{N},A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),0\le RHLinalg.frobSq(A)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/CartesianVariance.frobSq_nonneg (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every entry contributes a nonnegative square.

Definition 1.7 (Matrix Hilbert-space coordinates).

$$\forall n\in \mathbb{N},\mathrm{vectorize}\left(n\right)=LinearEquiv.trans(LinearEquiv.symm(LinearEquiv.curry(\mathbb{C},\mathbb{C},\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right))),LinearEquiv.symm(WithLp.linearEquiv(2,\mathbb{C},(\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(n\right))\to \mathbb{C})))$$

Formalization. D5/S3/Quantum/Matrix/CartesianVariance.vectorize (✓ std3).

Source. Repository-derived.

Commentary.

This complex linear equivalence arranges matrix entries by their ordered pair of indices. It composes Mathlib’s inverse currying equivalence with the inverse WithLp linear equivalence.

Theorem 1.8 (Vectorization preserves the Frobenius square).

$$\forall n\in \mathbb{N},A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),(\Vert \mathrm{vectorize}\left(n,A\right)\Vert {)}^2=RHLinalg.frobSq(A)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/CartesianVariance.vectorize_norm_sq (✓ std3). ∎

Source. Repository-derived.

Commentary.

The Euclidean norm sums the same entries.

Definition 1.9 (Cartesian variance).

$$\forall n\in \mathbb{N},A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),\mathrm{variance}\left(A,rho\right)=Complex.re(Matrix.trace(rho\cdot (\frac{1}{2}\cdot (Matrix.conjTranspose(A)\cdot A+A\cdot Matrix.conjTranspose(A)))))-Complex.normSq(Matrix.trace(rho\cdot A))$$

Formalization. D5/S3/Quantum/Matrix/CartesianVariance.variance (✓ std3).

Citation. Koenraad M. R. Audenaert (2009). Variance bounds, with an application to norm bounds for commutators. URL: https://arxiv.org/abs/0907.3913.

Commentary.

“Each modulus builds a different variance, which we’ll distinguish by the corresponding subscript too.” Equation (27), page 17, reads Var∗(X) = Tr[ρ|X|²∗] − |Tr[ρX]|², with subscript C giving |X|²C = (X∗X + XX∗)/2. Here X is A, and the real part makes the real-valued trace explicit.

Definition 1.10 (Cartesian quadratic matrix).

$$\forall n\in \mathbb{N},A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),\mathrm{cartesian}\left(A\right)=\frac{1}{2}\cdot (Matrix.conjTranspose(A)\cdot A+A\cdot Matrix.conjTranspose(A))$$

Formalization. D5/S3/Quantum/Matrix/CartesianVariance.cartesian (✓ std3).

Citation. Koenraad M. R. Audenaert (2009). Variance bounds, with an application to norm bounds for commutators. URL: https://arxiv.org/abs/0907.3913.

Commentary.

“For that reason we need a name for the expression ((X∗X + XX∗)/2)1/2, and we have chosen to call it the Cartesian modulus.” (page 17). This definition is the square of that modulus, the literal average of the two Gram matrices.

Theorem 1.11 (A pure vector attains the density maximum).

$$\forall n\in \mathbb{N},A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),0<n\Rightarrow \left(\exists v\in \mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left(n\right)\right),\Vert v\Vert =1\wedge \left(\forall rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),\left(Matrix.PosSemidef(rho)\wedge Matrix.trace(rho)=1\right)\Rightarrow \mathrm{variance}\left(A,rho\right)\le \mathrm{variance}\left(A,Matrix.vecMulVec(WithLp.ofLp(v),\mathrm{star}\left(WithLp.ofLp(v)\right))\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/CartesianVariance.pure_variance_maximizer (✓ std3). ∎

Citation. Koenraad M. R. Audenaert (2009). Variance bounds, with an application to norm bounds for commutators. URL: https://arxiv.org/abs/0907.3913.

Commentary.

A compact density set supplies a maximum. First-order optimality gives a linear Hermitian maximum; Toeplitz-Hausdorff on its top eigenspace preserves the complex mean while selecting a unit vector.

Theorem 1.12 (Hilbert-space trace pairing).

$$\forall n\in \mathbb{N},A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),B\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),\mathrm{inner}\left(\mathbb{C},\mathrm{vectorize}\left(n,A\right),\mathrm{vectorize}\left(n,B\right)\right)=Matrix.trace(Matrix.conjTranspose(A)\cdot B)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/CartesianVariance.matrix_pairing (✓ std3). ∎

Source. Repository-derived.

Commentary.

Vectorization realizes the trace inner product.

Theorem 1.13 (Conjugate-transpose invariance).

$$\forall n\in \mathbb{N},A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),RHLinalg.frobSq(Matrix.conjTranspose(A))=RHLinalg.frobSq(A)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/CartesianVariance.frobSq_star (✓ std3). ∎

Source. Repository-derived.

Commentary.

Conjugation preserves squared moduli and transpose permutes entries.

Theorem 1.14 (Trace-product Cauchy-Schwarz).

$$\forall n\in \mathbb{N},Q\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),B\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),Complex.normSq(Matrix.trace(Q\cdot B))\le RHLinalg.frobSq(Q)\cdot RHLinalg.frobSq(B)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/CartesianVariance.trace_product_cauchy (✓ std3). ∎

Source. Repository-derived.

Commentary.

Apply Hilbert-space Cauchy-Schwarz to Q conjugateTranspose and B.

Theorem 1.15 (The pure maximum bounds every commutator).

$$\forall n\in \mathbb{N},A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),v\in \mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left(n\right)\right),\left(\Vert v\Vert =1\wedge \left(\forall rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),\left(Matrix.PosSemidef(rho)\wedge Matrix.trace(rho)=1\right)\Rightarrow \mathrm{variance}\left(A,rho\right)\le \mathrm{variance}\left(A,Matrix.vecMulVec(WithLp.ofLp(v),\mathrm{star}\left(WithLp.ofLp(v)\right))\right)\right)\right)\Rightarrow \left(\forall B\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),RHLinalg.frobSq(\mathrm{commutator}\left(A,B\right))\le 4\cdot RHLinalg.frobSq(B)\cdot \mathrm{variance}\left(A,Matrix.vecMulVec(WithLp.ofLp(v),\mathrm{star}\left(WithLp.ofLp(v)\right))\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/CartesianVariance.commutator_pure_max_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

For nonzero B its two Gram matrices, normalized by twice the Frobenius square, form a density matrix. The commutator variance bound applies to this common density; B equal to zero is included.

References

• Truth anchor: D5/S3/Quantum/Matrix/CartesianVariance.cartesian
• Truth anchor: D5/S3/Quantum/Matrix/CartesianVariance.commutator_pure_max_bound
• Truth anchor: D5/S3/Quantum/Matrix/CartesianVariance.density_eigenvalues_sum
• Truth anchor: D5/S3/Quantum/Matrix/CartesianVariance.density_nonempty
• Truth anchor: D5/S3/Quantum/Matrix/CartesianVariance.frobSq_eq_sum
• Truth anchor: D5/S3/Quantum/Matrix/CartesianVariance.frobSq_nonneg
• Truth anchor: D5/S3/Quantum/Matrix/CartesianVariance.frobSq_star
• Truth anchor: D5/S3/Quantum/Matrix/CartesianVariance.hermitian_spectral_sum
• Truth anchor: D5/S3/Quantum/Matrix/CartesianVariance.matrix_pairing
• Truth anchor: D5/S3/Quantum/Matrix/CartesianVariance.psd_entry_bound
• Truth anchor: D5/S3/Quantum/Matrix/CartesianVariance.pure_variance_maximizer
• Truth anchor: D5/S3/Quantum/Matrix/CartesianVariance.trace_product_cauchy
• Truth anchor: D5/S3/Quantum/Matrix/CartesianVariance.variance
• Truth anchor: D5/S3/Quantum/Matrix/CartesianVariance.vectorize
• Truth anchor: D5/S3/Quantum/Matrix/CartesianVariance.vectorize_norm_sq
• Dependency: D5/S3/Observer/HiddenFlow/ProjectionCommutatorIdentity
• Dependency: D5/S3/Quantum/BlockNorm/EssentiallyHermitian
• Dependency: D5/S3/Quantum/Entanglement/UniversalReplacementCapacityGrowth
• Dependency: D5/S3/Quantum/Fibers/PhysicalFiber
• Dependency: D5/S3/Quantum/Matrix/NumericalRange