Compound matrices on HermitianMat

This file lifts the compound-matrix construction from QuantumInfo.ForMathlib.Majorization to HermitianMat. The compound matrix of a Hermitian matrix is again Hermitian, and inherits the natural spectral and positivity properties of the original.

noncomputable def HermitianMat.compoundHermitian {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (k : ℕ) : HermitianMat { S : Finset d // S.card = k } ℂ

The k-th compound matrix of a Hermitian matrix, packaged as a HermitianMat.

Equations

• A.compoundHermitian k = ⟨compoundMatrix (↑A) k, ⋯⟩

theorem HermitianMat.compoundHermitian_eigenvalues {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (k : ℕ) : ∃ (σ : { S : Finset d // S.card = k } ≃ { S : Finset d // S.card = k }), ⋯.eigenvalues ∘ ⇑σ = fun (S : { S : Finset d // S.card = k }) => ∏ i : Fin k, ⋯.eigenvalues (((↑S).orderEmbOfFin ⋯) i)

The eigenvalues of compoundHermitian A k are the products of eigenvalues of A over k-subsets, up to an index permutation.

theorem HermitianMat.compoundHermitian_nonneg {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (hA : 0 ≤ A) (k : ℕ) : 0 ≤ A.compoundHermitian k

compoundHermitian preserves positive semidefiniteness.

theorem HermitianMat.compoundHermitian_conj {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (B : Matrix d d ℂ) (k : ℕ) : ((conj B) A).compoundHermitian k = (conj (compoundMatrix B k)) (A.compoundHermitian k)

compoundHermitian distributes over HermitianMat.conj: the compound of A.conj B equals the conjugation of compoundHermitian A k by compoundMatrix B k.