structure Oseledets.OperatorEntropy.DensityMatrix (n : Type u_2) [Fintype n] [DecidableEq n] : Type u_2

A finite-dimensional density matrix over ℂ: a positive-semidefinite, unit-trace matrix.

• val : Matrix n n ℂ
• posSemidef : self.val.PosSemidef
• trace_one : self.val.trace = 1

noncomputable def Oseledets.OperatorEntropy.vonNeumannEntropy {n : Type u_1} [Fintype n] [DecidableEq n] (ρ : DensityMatrix n) : ℝ

The von Neumann entropy S(ρ) = ∑ᵢ negMulLog(λᵢ) over the (real) eigenvalues of ρ.

Equations

• Oseledets.OperatorEntropy.vonNeumannEntropy ρ = ∑ i : n, (⋯.eigenvalues i).negMulLog

theorem Oseledets.OperatorEntropy.DensityMatrix.eigenvalues_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] (ρ : DensityMatrix n) (i : n) : 0 ≤ ⋯.eigenvalues i

The eigenvalues of a density matrix are nonnegative.

theorem Oseledets.OperatorEntropy.DensityMatrix.sum_eigenvalues_eq_one {n : Type u_1} [Fintype n] [DecidableEq n] (ρ : DensityMatrix n) : ∑ i : n, ⋯.eigenvalues i = 1

The eigenvalues of a density matrix sum to 1 (its trace).

theorem Oseledets.OperatorEntropy.DensityMatrix.eigenvalues_le_one {n : Type u_1} [Fintype n] [DecidableEq n] (ρ : DensityMatrix n) (i : n) : ⋯.eigenvalues i ≤ 1

Each eigenvalue of a density matrix is at most 1.

theorem Oseledets.OperatorEntropy.vonNeumannEntropy_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] (ρ : DensityMatrix n) : 0 ≤ vonNeumannEntropy ρ

The von Neumann entropy of a density matrix is nonnegative.

noncomputable def Oseledets.OperatorEntropy.DensityMatrix.maximallyMixed {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] : DensityMatrix n

The maximally mixed state (dim)⁻¹ • I: a canonical inhabitant of DensityMatrix n for nonempty n, witnessing that the density-matrix API and the entropy bounds are non-vacuous.

Equations

• Oseledets.OperatorEntropy.DensityMatrix.maximallyMixed = { val := (↑(Fintype.card n))⁻¹ • 1, posSemidef := ⋯, trace_one := ⋯ }

@[implicit_reducible]

noncomputable instance Oseledets.OperatorEntropy.instInhabitedDensityMatrixFinOfNatNat : Inhabited (DensityMatrix (Fin 1))

Equations

• Oseledets.OperatorEntropy.instInhabitedDensityMatrixFinOfNatNat = { default := Oseledets.OperatorEntropy.DensityMatrix.maximallyMixed }