Unitary operators on quantum state

This file is intended for lemmas about unitary matrices (Matrix.unitaryGroup) and how they apply to Bras, Kets, and MState mixed states.

This is imported by CPTPMap to define things like unitary channels, Kraus operators, and complementary channels, so this file itself does not discuss channels yet.

def MState.«term𝐔[_]» : Lean.ParserDescr

Equations

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

def MState.U_conj {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (U : ↥𝐔[d]) : MState d

Conjugate a state by a unitary matrix (applying the unitary as an evolution).

Equations

• ρ.U_conj U = { toSubtype := ⟨↑U * ρ.m * ↑(star U), ⋯⟩, zero_le := ⋯, tr := ⋯ }

theorem MState.U_conj_spectrum_eq {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (U : ↥𝐔[d]) : ∃ (σ : d ≃ d), (ρ.U_conj U).spectrum = ρ.spectrum.relabel σ