Documentation

LeanPool.LeanQuantumAlg.Core.Components.Control

Controlled gates #

Gate.controlled U is the (1 + n)-qubit gate that applies the n-qubit gate U on the target register exactly when the control qubit is in |1>, and does nothing when it is in |0> [CEMM98, cemm6.tex:127]. As a matrix it is the block decomposition c-U = |0><0| ⊗ 1 + |1><1| ⊗ U.

The projectors proj0 and proj1 are HilbertOperators, not gates.

source
def QuantumAlg.Gate.proj0 :
HilbertOperator 1

The one-qubit projector |0><0| = [[1, 0], [0, 0]].

Equations
Instances For
    source
    def QuantumAlg.Gate.proj1 :
    HilbertOperator 1

    The one-qubit projector |1><1| = [[0, 0], [0, 1]].

    Equations
    Instances For
      source
      @[simp]
      theorem QuantumAlg.Gate.proj0_conjTranspose :
      Matrix.conjTranspose proj0 = proj0
      source
      @[simp]
      theorem QuantumAlg.Gate.proj1_conjTranspose :
      Matrix.conjTranspose proj1 = proj1
      source
      theorem QuantumAlg.Gate.proj0_mul_proj0 :
      proj0 * proj0 = proj0
      source
      theorem QuantumAlg.Gate.proj0_mul_proj1 :
      proj0 * proj1 = 0
      source
      theorem QuantumAlg.Gate.proj1_mul_proj0 :
      proj1 * proj0 = 0
      source
      theorem QuantumAlg.Gate.proj1_mul_proj1 :
      proj1 * proj1 = proj1
      source
      theorem QuantumAlg.Gate.proj0_add_proj1 :
      proj0 + proj1 = 1
      source
      @[simp]
      theorem QuantumAlg.Gate.proj0_applyVec_ket0 :
      proj0.applyVec PureState.ket0.vec = PureState.ket0.vec
      source
      @[simp]
      theorem QuantumAlg.Gate.proj0_applyVec_ket1 :
      proj0.applyVec PureState.ket1.vec = 0
      source
      @[simp]
      theorem QuantumAlg.Gate.proj1_applyVec_ket0 :
      proj1.applyVec PureState.ket0.vec = 0
      source
      @[simp]
      theorem QuantumAlg.Gate.proj1_applyVec_ket1 :
      proj1.applyVec PureState.ket1.vec = PureState.ket1.vec
      source
      noncomputable def QuantumAlg.Gate.controlledOp {n : ℕ} (U : Gate n) :
      HilbertOperator (1 + n)

      Raw controlled-operator matrix.

      Equations
      Instances For
        source
        noncomputable def QuantumAlg.Gate.controlled {n : ℕ} (U : Gate n) :
        Gate (1 + n)

        The controlled gate c-U.

        Equations
        Instances For
          source
          @[simp]
          theorem QuantumAlg.Gate.controlled_applyVec_ket0_tensor {n : ℕ} (U : Gate n) (psi : StateVector n) :
          U.controlled.op.applyVec (PureState.ket0.vec.tensor psi) = PureState.ket0.vec.tensor psi

          On the |0> control branch c-U does nothing.

          source
          @[simp]
          theorem QuantumAlg.Gate.controlled_applyVec_ket1_tensor {n : ℕ} (U : Gate n) (psi : StateVector n) :
          U.controlled.op.applyVec (PureState.ket1.vec.tensor psi) = PureState.ket1.vec.tensor (U.applyVec psi)

          On the |1> control branch c-U applies U.

          source
          @[simp]
          theorem QuantumAlg.Gate.controlled_apply_ket0_tensor {n : ℕ} (U : Gate n) (psi : PureState n) :
          U.controlled.apply (PureState.ket0.tensor psi) = PureState.ket0.tensor psi

          On the |0> control branch c-U does nothing.

          source
          @[simp]
          theorem QuantumAlg.Gate.controlled_apply_ket1_tensor {n : ℕ} (U : Gate n) (psi : PureState n) :
          U.controlled.apply (PureState.ket1.tensor psi) = PureState.ket1.tensor (U.apply psi)

          On the |1> control branch c-U applies U.

          source
          theorem QuantumAlg.Gate.controlled_mem_unitaryGroup {n : ℕ} {U : Gate n} (_hU : U.op ∈ Matrix.unitaryGroup (Fin (2 ^ n)) ℂ) :
          U.controlled.op ∈ Matrix.unitaryGroup (Fin (2 ^ (1 + n))) ℂ

          c-U is unitary.

          source
          theorem QuantumAlg.Gate.controlled_X :
          X.controlled = CNOT

          Sanity check: the controlled Pauli-X gate is exactly CNOT.