Unitary operators on quantum state #
This file is intended for lemmas about unitary matrices (Matrix.unitaryGroup
) and how they apply to
Bra
s, Ket
s, 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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Conjugate a state by a unitary matrix (applying the unitary as an evolution).
Equations
- ρ.U_conj U = { M := (HermitianMat.conj ↑U) ↑ρ, zero_le := ⋯, tr := ⋯ }
Instances For
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))
Instances For
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.
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.