Physlib

QuantumInfo.States.Mixed.MState

Finite dimensional quantum mixed states, ρ.

The same comments apply as in `Braket`:

These could be done with a Hilbert space of Fintype, which would look like ```lean4 (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [FiniteDimensional ℂ H] ``` or by choosing a particular `Basis` and asserting it is `Fintype`. But frankly it seems easier to mostly focus on the basis-dependent notion of `Matrix`, which has the added benefit of an obvious "classical" interpretation (as the basis elements, or diagonal elements of a mixed state). In that sense, this quantum theory comes with the a particular classical theory always preferred.

Important definitions: * `instMixable`: the `Mixable` instance allowing convex combinations of `MState`s * `ofClassical`: Mixed states representing classical distributions * `purity`: The purity `Tr[ρ^2]` of a state * `spectrum`: The spectrum of the matrix * `uniform`: The maximally mixed state * `mix`: The total state corresponding to an ensemble * `average`: Averages a function over an ensemble, with appropriate weights

2 declarations

theorem

⟨pure ψ,pure ϕ⟩=∣⟨ψ∣ϕ⟩∣2\langle \text{pure } \psi, \text{pure } \phi \rangle = |\langle \psi | \phi \rangle|^2

For any two kets ∣ψ⟩|\psi\rangle and ∣ϕ⟩|\phi\rangle in a finite-dimensional Hilbert space, the Hilbert-Schmidt inner product of their corresponding pure states ρψ=∣ψ⟩⟨ψ∣\rho_\psi = |\psi\rangle\langle\psi| and ρϕ=∣ϕ⟩⟨ϕ∣\rho_\phi = |\phi\rangle\langle\phi| is equal to the squared magnitude of the inner product of the kets: ⟨pure ψ,pure ϕ⟩Prob=∣⟨ψ∣ϕ⟩∣2\langle \text{pure } \psi, \text{pure } \phi \rangle_{\text{Prob}} = |\langle \psi | \phi \rangle|^2 where ⟨⋅,⋅⟩Prob\langle \cdot, \cdot \rangle_{\text{Prob}} denotes the inner product on the space of mixed states.

theorem

The trace norm of a quantum mixed state is 1 (∥ρ∥tr=1\|\rho\|_{\text{tr}} = 1)

For any quantum mixed state ρ\rho of finite dimension dd, let MM be its underlying d×dd \times d complex matrix representation. The trace norm of MM is equal to 1, i.e., ∥M∥tr=1\|M\|_{\text{tr}} = 1.