Density-state covariance and its sparse sum

Abstract

For a finite-dimensional density state, symmetrized covariance satisfies Cauchy-Schwarz. A spectral interval of half width Delta and sparse row supports bound the total absolute covariance.

Definition 1.1 (Real expectation).

$$E\left(\rho ,A\right)=\Re \mathrm{tr}\left(\rho A\right)$$

Formalization. D5/S3/Quantum/Information/CovarianceSumBound.expectation (✓ std3).

Citation. Paolo Gibilisco, Fumio Hiai, Denes Petz (2007). Quantum covariance, quantum Fisher information and the uncertainty principle. URL: https://arxiv.org/abs/0712.1208.

Commentary.

The state is a positive semidefinite complex matrix of trace one. All carriers are arbitrary finite types; singular states are included.

Definition 1.2 (Symmetrized covariance).

$$\mathrm{Cov}\left(\rho ,A,B\right)=\frac{E\left(\rho ,AB\right)+E\left(\rho ,BA\right)}{2}-E\left(\rho ,A\right)E\left(\rho ,B\right)$$

Formalization. D5/S3/Quantum/Information/CovarianceSumBound.covariance (✓ std3).

Citation. Paolo Gibilisco, Fumio Hiai, Denes Petz (2007). Quantum covariance, quantum Fisher information and the uncertainty principle. URL: https://arxiv.org/abs/0712.1208.

Commentary.

For Hermitian A and B this is one half the expectation of AB+BA minus the product of expectations. A and B need not commute.

Definition 1.3 (Variance).

$$\mathrm{Var}\left(\rho ,A\right)=E\left(\rho ,A^2\right)-{E\left(\rho ,A\right)}^2$$

Formalization. D5/S3/Quantum/Information/CovarianceSumBound.variance (✓ std3).

Citation. Paolo Gibilisco, Fumio Hiai, Denes Petz (2007). Quantum covariance, quantum Fisher information and the uncertainty principle. URL: https://arxiv.org/abs/0712.1208.

Commentary.

Variance uses the same state and the same expectation as covariance.

Theorem 1.4 (Symmetry).

$$\mathrm{Cov}\left(\rho ,A,B\right)=\mathrm{Cov}\left(\rho ,B,A\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Information/CovarianceSumBound.covariance_symm (✓ std3). ∎

Citation. Paolo Gibilisco, Fumio Hiai, Denes Petz (2007). Quantum covariance, quantum Fisher information and the uncertainty principle. URL: https://arxiv.org/abs/0712.1208.

Commentary.

Exchanging the two observables preserves symmetrized covariance.

Theorem 1.5 (Right additivity).

$$\mathrm{Cov}\left(\rho ,A,B+C\right)=\mathrm{Cov}\left(\rho ,A,B\right)+\mathrm{Cov}\left(\rho ,A,C\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Information/CovarianceSumBound.covariance_add_right (✓ std3). ∎

Citation. Denes Petz (2001). Covariance and Fisher information in quantum mechanics. URL: https://arxiv.org/abs/quant-ph/0106125.

Commentary.

For every fixed state and A, covariance is additive in its right argument.

Theorem 1.6 (Self-covariance is variance).

$$\mathrm{Cov}\left(\rho ,A,A\right)=\mathrm{Var}\left(\rho ,A\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Information/CovarianceSumBound.covariance_self (✓ std3). ∎

Citation. Paolo Gibilisco, Fumio Hiai, Denes Petz (2007). Quantum covariance, quantum Fisher information and the uncertainty principle. URL: https://arxiv.org/abs/0712.1208.

Commentary.

The two definitions agree on equal observables.

Theorem 1.7 (Variance is nonnegative).

$$0\le \mathrm{Var}\left(\rho ,A\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Information/CovarianceSumBound.variance_nonneg (✓ std3). ∎

Citation. Denes Petz (2001). Covariance and Fisher information in quantum mechanics. URL: https://arxiv.org/abs/quant-ph/0106125.

Commentary.

For a Hermitian observable, its centered square has nonnegative expectation.

Theorem 1.8 (Cauchy-Schwarz in a density state).

$$|\mathrm{Cov}\left(\rho ,A,B\right)|\le \sqrt{\mathrm{Var}\left(\rho ,A\right)\mathrm{Var}\left(\rho ,B\right)}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Information/CovarianceSumBound.abs_covariance_le (✓ std3). ∎

Citation. Mathlib contributors (2026). Weighted matrix inner products and bounded variances in Mathlib. URL: https://github.com/leanprover-community/mathlib4/blob/v4.33.0/Mathlib/Analysis/Matrix/Order.lean.

Commentary.

For Hermitian A and B, centered observables belong to the weighted matrix semi-inner product space. Its real pairing is exactly covariance.

Theorem 1.9 (Spectral half-width bound).

$$\mathrm{Var}\left(\rho ,A\right)\le {\Delta }^2$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Information/CovarianceSumBound.variance_le_half_width_sq (✓ std3). ∎

Citation. Mathlib contributors (2026). Weighted matrix inner products and bounded variances in Mathlib. URL: https://github.com/leanprover-community/mathlib4/blob/v4.33.0/Mathlib/Analysis/Matrix/Order.lean.

Commentary.

Assume Delta is nonnegative and every spectral value of Hermitian A lies in [c-Delta,c+Delta]. Delta is the half width. Continuous functional calculus bounds the square centered at c, and subtracting the squared mean displacement bounds the variance.

Theorem 1.10 (Sum from variance bounds).

$$\sum _{x,y\in Q}|\mathrm{Cov}\left(\rho ,R\left(x\right),R\left(y\right)\right)|\le \mathrm{card}\left(Q\right)b{\Delta }^2$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Information/CovarianceSumBound.covariance_sum_le_of_variance (✓ std3). ∎

Citation. Sheldon Axler (2024). Linear Algebra Done Right, fourth edition. URL: https://linear.axler.net/.

Commentary.

On a finite set Q, assume every R(x) is Hermitian, each variance is at most Delta squared, and for each x in Q at most b elements y in Q have nonzero covariance. Summing only these supports gives the bound.

Theorem 1.11 (Sparse covariance sum bound).

$$\sum _{x,y\in Q}|\mathrm{Cov}\left(\rho ,R\left(x\right),R\left(y\right)\right)|\le \mathrm{card}\left(Q\right)b{\Delta }^2$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Information/CovarianceSumBound.covariance_sum_le (✓ std3). ∎

Citation. Rajesh Sharma, M. Gupta, G. Kapoor (2010). Some better bounds on the variance with applications. URL: https://jmi.ele-math.com/04-32/Some-better-bounds-on-the-variance-with-applications.

Commentary.

For a finite set Q and a density state, assume all R(x), x in Q, are Hermitian with spectra in [c(x)-Delta,c(x)+Delta], where Delta is nonnegative. For every x in Q the support of y mapped to Cov(R(x),R(y)) has at most b elements in Q. Then the bound follows with N equal to card Q. The support hypothesis is the locality input; the theorem does not derive a propagation or preparation-time bound.

References

• Truth anchor: D5/S3/Quantum/Information/CovarianceSumBound.abs_covariance_le
• Truth anchor: D5/S3/Quantum/Information/CovarianceSumBound.covariance
• Truth anchor: D5/S3/Quantum/Information/CovarianceSumBound.covariance_add_right
• Truth anchor: D5/S3/Quantum/Information/CovarianceSumBound.covariance_self
• Truth anchor: D5/S3/Quantum/Information/CovarianceSumBound.covariance_sum_le
• Truth anchor: D5/S3/Quantum/Information/CovarianceSumBound.covariance_sum_le_of_variance
• Truth anchor: D5/S3/Quantum/Information/CovarianceSumBound.covariance_symm
• Truth anchor: D5/S3/Quantum/Information/CovarianceSumBound.expectation
• Truth anchor: D5/S3/Quantum/Information/CovarianceSumBound.variance
• Truth anchor: D5/S3/Quantum/Information/CovarianceSumBound.variance_le_half_width_sq
• Truth anchor: D5/S3/Quantum/Information/CovarianceSumBound.variance_nonneg
• Dependency: D5/S3/Quantum/Divergence/QuantumRelativeEntropyDefectComposition