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

(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 MStates
• 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
• MEnsemble and PEnsemble: Ensemble of mixed and pure states, respectively
• mix: The total state corresponding to an ensemble
• average: Averages a function over an ensemble, with appropriate weights

structure MState (d : Type u_1) [Fintype d] extends ↥(selfAdjoint (Matrix d d ℂ)) : Type u_1

A mixed state as a PSD matrix with trace 1.

• val : Matrix d d ℂ
• property : ↑self.toSubtype ∈ selfAdjoint (Matrix d d ℂ)
• zero_le : 0 ≤ self.toSubtype
• tr : (↑self.toSubtype).trace = 1

def MState.m {d : Type u_1} [Fintype d] (ρ : MState d) : Matrix d d ℂ

The underlying Matrix in an MState

Equations

• ρ.m = ↑ρ.toSubtype

@[reducible]

def MState.M {d : Type u_1} [Fintype d] (ρ : MState d) : HermitianMat d ℂ

The underlying HermitianMat in an MState

Equations

• ↑ρ = ρ.toSubtype

instance MState.instCoe {d : Type u_1} [Fintype d] : Coe (MState d) (HermitianMat d ℂ)

Equations

• MState.instCoe = { coe := MState.M }

@[simp]

theorem MState.tr' {d : Type u_1} [Fintype d] (ρ : MState d) : (↑ρ).trace = 1

@[simp]

theorem MState.toSubtype_eq_coe {d : Type u_1} [Fintype d] (ρ : MState d) : ρ.toSubtype = ↑ρ

theorem MState.ext {d : Type u_1} [Fintype d] {ρ₁ ρ₂ : MState d} (h : ↑ρ₁ = ↑ρ₂) : ρ₁ = ρ₂

theorem MState.pos {d : Type u_1} [Fintype d] (ρ : MState d) : (↑ρ.toSubtype).PosSemidef

theorem MState.Hermitian {d : Type u_1} [Fintype d] (ρ : MState d) : ρ.m.IsHermitian

Every mixed state is Hermitian.

theorem MState.ext_m {d : Type u_1} [Fintype d] {ρ₁ ρ₂ : MState d} (h : ρ₁.m = ρ₂.m) : ρ₁ = ρ₂

theorem MState.toMat_inj {d : Type u_1} [Fintype d] : Function.Injective m

The map from mixed states to their matrices is injective

theorem MState.convex (d : Type u_1) [Fintype d] : Convex ℝ (Set.range m)

The matrices corresponding to MStates are Convex ℝ

instance MState.instMixable {d : Type u_1} [Fintype d] : Mixable (Matrix d d ℂ) (MState d)

Equations

• MState.instMixable = { to_U := MState.m, to_U_inj := ⋯, convex := ⋯, mkT := fun {u : Matrix d d ℂ} (h : ∃ (t : MState d), t.m = u) => ⟨{ toSubtype := ⟨u, ⋯⟩, zero_le := ⋯, tr := ⋯ }, ⋯⟩ }

instance MState.nonempty {d : Type u_1} [Fintype d] (ρ : MState d) : Nonempty d

theorem MState.PosSemidef_outer_self_conj {d : Type u_1} [Fintype d] (v : d → ℂ) : (Matrix.vecMulVec v ((starRingEnd (d → ℂ)) v)).PosSemidef

def MState.inner {d : Type u_1} [Fintype d] (ρ σ : MState d) : Prob

The inner product of two MState's, as a real number between 0 and 1.

Equations

• ρ.inner σ = ⟨(↑ρ).inner ↑σ, ⋯⟩

def MState.exp_val_ℂ {d : Type u_1} [Fintype d] (T : Matrix d d ℂ) (ρ : MState d) : ℂ

Equations

• MState.exp_val_ℂ T ρ = (T * ρ.m).trace

def MState.exp_val {d : Type u_1} [Fintype d] (T : HermitianMat d ℂ) (ρ : MState d) : ℝ

Equations

• MState.exp_val T ρ = (↑ρ).inner T

theorem MState.exp_val_nonneg {d : Type u_1} [Fintype d] {T : HermitianMat d ℂ} (h : 0 ≤ T) (ρ : MState d) : 0 ≤ exp_val T ρ

theorem MState.exp_val_le_one {d : Type u_1} [Fintype d] [DecidableEq d] {T : HermitianMat d ℂ} (h : T ≤ 1) (ρ : MState d) : exp_val T ρ ≤ 1

theorem MState.exp_val_prob {d : Type u_1} [Fintype d] [DecidableEq d] {T : HermitianMat d ℂ} (h : 0 ≤ T ∧ T ≤ 1) (ρ : MState d) : 0 ≤ exp_val T ρ ∧ exp_val T ρ ≤ 1

def MState.pure {d : Type u_1} [Fintype d] (ψ : Ket d) : MState d

A mixed state can be constructed as a pure state arising from a ket.

Equations

• MState.pure ψ = { toSubtype := ⟨Matrix.vecMulVec ⇑ψ ⇑↑ψ, ⋯⟩, zero_le := ⋯, tr := ⋯ }

@[simp]

theorem MState.pure_of {d : Type u_1} [Fintype d] {i j : d} (ψ : Ket d) : (pure ψ).m i j = ψ i * (starRingEnd ℂ) (ψ j)

def MState.purity {d : Type u_1} [Fintype d] (ρ : MState d) : Prob

The purity of a state is Tr[ρ^2]. This is a Prob, because it is always between zero and one.

Equations

• ρ.purity = ⟨(↑ρ).inner ↑ρ, ⋯⟩

def MState.spectrum {d : Type u_1} [Fintype d] (ρ : MState d) : Distribution d

The eigenvalue spectrum of a mixed quantum state, as a Distribution.

Equations

• ρ.spectrum = Distribution.mk' (fun (x : d) => ⋯.eigenvalues x) ⋯ ⋯

theorem MState.spectrum_pure_eq_constant {d : Type u_1} [Fintype d] (ψ : Ket d) : ∃ (i : d), (pure ψ).spectrum = Distribution.constant i

The specturm of a pure state is (1,0,0,...), i.e. a constant distribution.

theorem MState.pure_of_constant_spectrum {d : Type u_1} [Fintype d] (ρ : MState d) (h : ∃ (i : d), ρ.spectrum = Distribution.constant i) : ∃ (ψ : Ket d), ρ = pure ψ

If the specturm of a mixed state is (1,0,0...) i.e. a constant distribution, it is a pure state.

theorem MState.pure_iff_constant_spectrum {d : Type u_1} [Fintype d] (ρ : MState d) : (∃ (ψ : Ket d), ρ = pure ψ) ↔ ∃ (i : d), ρ.spectrum = Distribution.constant i

A state ρ is pure iff its spectrum is (1,0,0,...) i.e. a constant distribution.

theorem MState.pure_iff_purity_one {d : Type u_1} [Fintype d] (ρ : MState d) : (∃ (ψ : Ket d), ρ = pure ψ) ↔ ρ.purity = 1

def MState.prod {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] (ρ₁ : MState d₁) (ρ₂ : MState d₂) : MState (d₁ × d₂)

Equations

• (ρ₁⊗ρ₂) = { toSubtype := ⟨Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ρ₁.m ρ₂.m, ⋯⟩, zero_le := ⋯, tr := ⋯ }

def MState.«term_⊗_» : Lean.TrailingParserDescr

Equations

• MState.«term_⊗_» = Lean.ParserDescr.trailingNode `MState.«term_⊗_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊗") (Lean.ParserDescr.cat `term 0))

theorem MState.pure_prod_pure {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] (ψ₁ : Ket d₁) (ψ₂ : Ket d₂) : pure (ψ₁⊗ψ₂) = pure ψ₁⊗pure ψ₂

The product of pure states is a pure product state , Ket.prod.

def MState.ofClassical {d : Type u_1} [Fintype d] (dist : Distribution d) : MState d

A representation of a classical distribution as a quantum state, diagonal in the given basis.

Equations

• MState.ofClassical dist = { toSubtype := ⟨Matrix.diagonal fun (x : d) => ↑↑(dist x), ⋯⟩, zero_le := ⋯, tr := ⋯ }

def MState.uniform {d : Type u_1} [Fintype d] [Nonempty d] : MState d

The maximally mixed state.

Equations

• MState.uniform = MState.ofClassical Distribution.uniform

instance MState.instUnique {d : Type u_1} [Fintype d] [Unique d] : Unique (MState d)

There is exactly one state on a dimension-1 system.

Equations

• MState.instUnique = { default := MState.uniform, uniq := ⋯ }

instance MState.instInhabited {d : Type u_1} [Fintype d] [Nonempty d] : Inhabited (MState d)

There exists a mixed state for every nonempty d. Here, the maximally mixed one is chosen.

Equations

• MState.instInhabited = { default := MState.uniform }

def MState.traceLeft {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] (ρ : MState (d₁ × d₂)) : MState d₂

Partial tracing out the left half of a system.

Equations

• ρ.traceLeft = { toSubtype := ⟨ρ.m.traceLeft, ⋯⟩, zero_le := ⋯, tr := ⋯ }

def MState.traceRight {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] (ρ : MState (d₁ × d₂)) : MState d₁

Partial tracing out the right half of a system.

Equations

• ρ.traceRight = { toSubtype := ⟨ρ.m.traceRight, ⋯⟩, zero_le := ⋯, tr := ⋯ }

@[simp]

theorem MState.traceLeft_prod_eq {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] (ρ₁ : MState d₁) (ρ₂ : MState d₂) : (ρ₁⊗ρ₂).traceLeft = ρ₂

Taking the direct product on the left and tracing it back out gives the same state.

@[simp]

theorem MState.traceRight_prod_eq {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] (ρ₁ : MState d₁) (ρ₂ : MState d₂) : (ρ₁⊗ρ₂).traceRight = ρ₁

Taking the direct product on the right and tracing it back out gives the same state.

theorem MState.spectrum_prod {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] (ρ₁ : MState d₁) (ρ₂ : MState d₂) : ∃ (σ : d₁ × d₂ ≃ d₁ × d₂), ∀ (i : d₁) (j : d₂), (ρ₁⊗ρ₂).spectrum (σ (i, j)) = ρ₁.spectrum i * ρ₂.spectrum j

Spectrum of direct product. There is a permutation σ so that the spectrum of the direct product of ρ₁ and ρ₂, as permuted under σ, is the pairwise products of the spectra of ρ₁ and ρ₂.

def MState.IsSeparable {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] (ρ : MState (d₁ × d₂)) : Prop

A mixed state is separable iff it can be written as a convex combination of product mixed states.

Equations

• One or more equations did not get rendered due to their size.

theorem MState.IsSeparable_prod {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] (ρ₁ : MState d₁) (ρ₂ : MState d₂) : (ρ₁⊗ρ₂).IsSeparable

A product state MState.prod is separable.

theorem MState.pure_separable_iff_IsProd {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] (ψ : Ket (d₁ × d₂)) : (pure ψ).IsSeparable ↔ ψ.IsProd

A pure state is separable iff the ket is a product state.

theorem MState.pure_separable_iff_traceLeft_pure {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] (ψ : Ket (d₁ × d₂)) : (pure ψ).IsSeparable ↔ ∃ (ψ₁ : Ket d₂), pure ψ₁ = (pure ψ).traceLeft

A pure state is separable iff the partial trace on the left is pure.

def MState.purify {d : Type u_1} [Fintype d] (ρ : MState d) : Ket (d × d)

The purification of a mixed state. Always uses the full dimension of the Hilbert space (d) to purify, so e.g. an existing pure state with d=4 still becomes d=16 in the purification. The defining property is MState.traceRight_of_purify; see also MState.purify' for the bundled version.

Equations

• ρ.purify = { vec := fun (x : d × d) => match x with | (i, j) => let ρ2 := ↑⋯.eigenvectorUnitary i j; ρ2 * ↑√(⋯.eigenvalues j), normalized' := ⋯ }

@[simp]

theorem MState.purify_spec {d : Type u_1} [Fintype d] (ρ : MState d) : (pure ρ.purify).traceRight = ρ

The defining property of purification, that tracing out the purifying system gives the original mixed state.

def MState.purifyX {d : Type u_1} [Fintype d] (ρ : MState d) : { ψ : Ket (d × d) // (pure ψ).traceRight = ρ }

MState.purify bundled with its defining property MState.traceRight_of_purify.

Equations

• ρ.purifyX = ⟨ρ.purify, ⋯⟩

def MState.relabel {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] (ρ : MState d₁) (e : d₂ ≃ d₁) : MState d₂

Equations

• ρ.relabel e = { toSubtype := ⟨(Matrix.reindex e.symm e.symm) ρ.m, ⋯⟩, zero_le := ⋯, tr := ⋯ }

@[simp]

theorem MState.relabel_m {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] (ρ : MState d₁) (e : d₂ ≃ d₁) : (ρ.relabel e).m = ρ.m.submatrix ⇑e ⇑e

def MState.SWAP {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] (ρ : MState (d₁ × d₂)) : MState (d₂ × d₁)

The heterogeneous SWAP gate that exchanges the left and right halves of a quantum system. This can apply even when the two "halves" are of different types, as opposed to (say) the SWAP gate on quantum circuits that leaves the qubit dimensions unchanged. Notably, it is not unitary.

Equations

• ρ.SWAP = ρ.relabel (Equiv.prodComm d₁ d₂).symm

def MState.spectrum_SWAP {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] (ρ : MState (d₁ × d₂)) : ∃ (e : d₁ × d₂ ≃ d₂ × d₁), ρ.SWAP.spectrum.relabel e = ρ.spectrum

Equations

• ⋯ = ⋯

@[simp]

theorem MState.SWAP_SWAP {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] (ρ : MState (d₁ × d₂)) : ρ.SWAP.SWAP = ρ

@[simp]

theorem MState.traceLeft_SWAP {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] (ρ : MState (d₁ × d₂)) : ρ.SWAP.traceLeft = ρ.traceRight

@[simp]

theorem MState.traceRight_SWAP {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] (ρ : MState (d₁ × d₂)) : ρ.SWAP.traceRight = ρ.traceLeft

def MState.assoc {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] (ρ : MState ((d₁ × d₂) × d₃)) : MState (d₁ × d₂ × d₃)

The associator that re-clusters the parts of a quantum system.

Equations

• ρ.assoc = ρ.relabel (Equiv.prodAssoc d₁ d₂ d₃).symm

def MState.assoc' {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] (ρ : MState (d₁ × d₂ × d₃)) : MState ((d₁ × d₂) × d₃)

The associator that re-clusters the parts of a quantum system.

Equations

• ρ.assoc' = ρ.SWAP.assoc.SWAP.assoc.SWAP

@[simp]

theorem MState.assoc_assoc' {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] (ρ : MState (d₁ × d₂ × d₃)) : ρ.assoc'.assoc = ρ

@[simp]

theorem MState.assoc'_assoc {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] (ρ : MState ((d₁ × d₂) × d₃)) : ρ.assoc.assoc' = ρ

@[simp]

theorem MState.traceLeft_right_assoc {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] (ρ : MState ((d₁ × d₂) × d₃)) : ρ.assoc.traceLeft.traceRight = ρ.traceRight.traceLeft

@[simp]

theorem MState.traceRight_left_assoc' {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] (ρ : MState (d₁ × d₂ × d₃)) : ρ.assoc'.traceRight.traceLeft = ρ.traceLeft.traceRight

@[simp]

theorem MState.traceRight_assoc {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] (ρ : MState ((d₁ × d₂) × d₃)) : ρ.assoc.traceRight = ρ.traceRight.traceRight

@[simp]

theorem MState.traceLeft_assoc' {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] (ρ : MState (d₁ × d₂ × d₃)) : ρ.assoc'.traceLeft = ρ.traceLeft.traceLeft

@[simp]

theorem MState.traceLeft_left_assoc {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] (ρ : MState ((d₁ × d₂) × d₃)) : ρ.assoc.traceLeft.traceLeft = ρ.traceLeft

@[simp]

theorem MState.traceRight_right_assoc' {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] (ρ : MState (d₁ × d₂ × d₃)) : ρ.assoc'.traceRight.traceRight = ρ.traceRight

@[simp]

theorem MState.traceNorm_eq_1 {d : Type u_1} [Fintype d] (ρ : MState d) : ρ.m.traceNorm = 1

instance MState.instTopoMState {d : Type u_1} [Fintype d] : TopologicalSpace (MState d)

Mixed states inherit the subspace topology from matrices

Equations

• MState.instTopoMState = TopologicalSpace.induced MState.m instTopologicalSpaceMatrix

theorem MState.toMat_IsEmbedding {d : Type u_1} [Fintype d] : Topology.IsEmbedding m

The projection from mixed states to their matrices is an embedding

instance MState.instT5MState {d : Type u_1} [Fintype d] : T3Space (MState d)

def MState.piProd {ι : Type u} [DecidableEq ι] [fι : Fintype ι] {dI : ι → Type v} [(i : ι) → Fintype (dI i)] (ρi : (i : ι) → MState (dI i)) : MState ((i : ι) → dI i)

Equations

• MState.piProd ρi = { toSubtype := ⟨fun (j k : (i : ι) → dI i) => ∏ i : ι, (ρi i).m (j i) (k i), ⋯⟩, zero_le := ⋯, tr := ⋯ }

def MState.npow {d : Type u_1} [Fintype d] (ρ : MState d) (n : ℕ) : MState (Fin n → d)

Equations

• (ρ⊗^n) = MState.piProd fun (x : Fin n) => ρ

def MState.«term_⊗^_» : Lean.TrailingParserDescr

Equations

• MState.«term_⊗^_» = Lean.ParserDescr.trailingNode `MState.«term_⊗^_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊗^") (Lean.ParserDescr.cat `term 0))