Documentation

MIPRE.LCS.Pauli

Pauli Matrices #

This module defines the single-qubit Pauli matrices Pauli.I, Pauli.X, Pauli.Y, Pauli.Z, together with their multiplication table, anticommutation relations, and observable structure. It also records the Kronecker-product lemmas used to combine commuting or anticommuting pairs into commuting two-qubit observables.

source
def MIPRE.LCS.Pauli.I :
Matrix (Fin 2) (Fin 2) ℂ

The 2 × 2 identity matrix.

Equations
Instances For
    source
    def MIPRE.LCS.Pauli.X :
    Matrix (Fin 2) (Fin 2) ℂ

    The Pauli X (bit-flip) matrix.

    Equations
    Instances For
      source
      def MIPRE.LCS.Pauli.Y :
      Matrix (Fin 2) (Fin 2) ℂ

      The Pauli Y matrix.

      Equations
      Instances For
        source
        def MIPRE.LCS.Pauli.Z :
        Matrix (Fin 2) (Fin 2) ℂ

        The Pauli Z (phase-flip) matrix.

        Equations
        Instances For
          source
          theorem MIPRE.LCS.Pauli.I_eq_one :
          I = 1
          source
          theorem MIPRE.LCS.Pauli.I_comm_left (P : Matrix (Fin 2) (Fin 2) ℂ) :
          Commute I P
          source
          theorem MIPRE.LCS.Pauli.I_comm_right (P : Matrix (Fin 2) (Fin 2) ℂ) :
          Commute P I
          source
          theorem MIPRE.LCS.Pauli.I_mul_self :
          I * I = 1
          source
          theorem MIPRE.LCS.Pauli.X_mul_self :
          X * X = 1
          source
          theorem MIPRE.LCS.Pauli.Y_mul_self :
          Y * Y = 1
          source
          theorem MIPRE.LCS.Pauli.Z_mul_self :
          Z * Z = 1
          source
          theorem MIPRE.LCS.Pauli.star_I :
          star I = I
          source
          theorem MIPRE.LCS.Pauli.star_X :
          star X = X
          source
          theorem MIPRE.LCS.Pauli.star_Y :
          star Y = Y
          source
          theorem MIPRE.LCS.Pauli.star_Z :
          star Z = Z
          source
          theorem MIPRE.LCS.Pauli.X_mul_Y :
          X * Y = Complex.I • Z
          source
          theorem MIPRE.LCS.Pauli.Y_mul_X :
          Y * X = -Complex.I • Z
          source
          theorem MIPRE.LCS.Pauli.X_mul_Z :
          X * Z = -Complex.I • Y
          source
          theorem MIPRE.LCS.Pauli.Z_mul_X :
          Z * X = Complex.I • Y
          source
          theorem MIPRE.LCS.Pauli.Y_mul_Z :
          Y * Z = Complex.I • X
          source
          theorem MIPRE.LCS.Pauli.Z_mul_Y :
          Z * Y = -Complex.I • X
          source
          theorem MIPRE.LCS.Pauli.X_anticomm_Y :
          X * Y = -(Y * X)
          source
          theorem MIPRE.LCS.Pauli.X_anticomm_Z :
          X * Z = -(Z * X)
          source
          theorem MIPRE.LCS.Pauli.Y_anticomm_Z :
          Y * Z = -(Z * Y)
          source
          theorem MIPRE.LCS.Pauli.isObservable_I :
          IsObservable I
          source
          theorem MIPRE.LCS.Pauli.isObservable_X :
          IsObservable X
          source
          theorem MIPRE.LCS.Pauli.isObservable_Y :
          IsObservable Y
          source
          theorem MIPRE.LCS.Pauli.isObservable_Z :
          IsObservable Z
          source
          theorem MIPRE.LCS.commute_kronecker_of_commute {A B C D : Matrix (Fin 2) (Fin 2) ℂ} (hAC : Commute A C) (hBD : Commute B D) :
          Commute (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) C D)
          source
          theorem MIPRE.LCS.commute_kronecker_of_anticomm {A B C D : Matrix (Fin 2) (Fin 2) ℂ} (hAC : A * C = -(C * A)) (hBD : B * D = -(D * B)) :
          Commute (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) C D)
          source
          theorem MIPRE.LCS.IsObservable.kronecker {A B : Matrix (Fin 2) (Fin 2) ℂ} (hA : IsObservable A) (hB : IsObservable B) :
          IsObservable (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B)