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 «term𝐔[_]» : Lean.ParserDescr

Equations

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

@[simp]

theorem HermitianMat.trace_conj_unitary {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (A : HermitianMat n 𝕜) (U : ↥(Matrix.unitaryGroup n 𝕜)) : ((conj ↑U) A).trace = A.trace

@[simp]

theorem HermitianMat.le_conj_unitary {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (A B : HermitianMat n 𝕜) (U : ↥(Matrix.unitaryGroup n 𝕜)) : (conj ↑U) A ≤ (conj ↑U) B ↔ A ≤ B

@[simp]

theorem HermitianMat.inner_conj_unitary {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (A B : HermitianMat n 𝕜) (U : ↥(Matrix.unitaryGroup n 𝕜)) : ((conj ↑U) A).inner ((conj ↑U) B) = A.inner B

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 = { M := (HermitianMat.conj ↑U) ↑ρ, zero_le := ⋯, tr := ⋯ }

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

MState.U_conj, the action of a unitary on a mixed state by conjugation. The ◃ notation comes from the theory of racks and quandles, where this is a conjugation-like operation.

Equations

• MState.«term_◃_» = Lean.ParserDescr.trailingNode `MState.«term_◃_» 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◃ ") (Lean.ParserDescr.cat `term 81))

@[simp]

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

You might think this should only be true up to permutation, so that it would read like ∃ σ : Equiv.Perm d, (ρ.U_conj U).spectrum = ρ.spectrum.relabel σ. But since eigenvalues of a matrix are always canonically sorted, this is actually an equality.

@[simp]

theorem MState.inner_U_conj {d : Type u_1} [Fintype d] [DecidableEq d] (ρ σ : MState d) (U : ↥𝐔[d]) : (ρ.U_conj U).inner (σ.U_conj U) = ρ.inner σ

theorem MState.no_cloning {d : Type u_1} [Fintype d] [DecidableEq d] {ψ φ f : Ket d} {U : ↥𝐔[d × d]} (hψ : (pure (ψ ⊗ f)).U_conj U = pure (ψ ⊗ ψ)) (hφ : (pure (φ ⊗ f)).U_conj U = pure (φ ⊗ φ)) (H : ↑((pure ψ).inner (pure φ)) < 1) : ↑((pure ψ).inner (pure φ)) = 0

The No-cloning theorem, saying that if states ψ and φ can both be perfectly cloned using a unitary U and a fiducial state f, and they aren't identical (their inner product is less than 1), then the two states must be orthogonal to begin with. In short: only orthogonal states can be simultaneously cloned.