Documentation

QuantumInfo.Finite.Unitary

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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[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]) :

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

    Equations
    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
      Instances For
        @[simp]
        theorem MState.U_conj_spectrum_eq {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (U : 𝐔[d]) :

        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]} ( : (pure (ψ f)).U_conj U = pure (ψ ψ)) ( : (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.