Documentation

LeanPool.LeanQuantumAlg.Core.Components.Kets

Named one-qubit kets #

The standard one-qubit computational- and Hadamard-basis kets, as named instances of the generic basis ket LeanPool.LeanQuantumAlg.PureState.ket:

|0>, |1>, |+> = (|0> + |1>)/sqrt 2, and |-> = (|0> - |1>)/sqrt 2.

Linear combinations are formed at the raw StateVector layer and then bundled as PureState values once their unit norm has been proved.

source
def QuantumAlg.PureState.ket0 :
PureState 1

|0>, the first one-qubit basis ket.

Equations
Instances For
    source
    def QuantumAlg.PureState.ket1 :
    PureState 1

    |1>, the second one-qubit basis ket.

    Equations
    Instances For
      source
      noncomputable def QuantumAlg.PureState.invSqrt2 :
      ℂ

      (sqrt 2)^-1 : ℂ, the ubiquitous normalization scalar.

      Equations
      Instances For
        source
        @[simp]
        theorem QuantumAlg.PureState.invSqrt2_mul_self :
        invSqrt2 * invSqrt2 = 2⁻¹
        source
        @[simp]
        theorem QuantumAlg.PureState.invSqrt2_sq :
        invSqrt2 ^ 2 = 2⁻¹
        source
        @[simp]
        theorem QuantumAlg.PureState.invSqrt2_mul_mul_invSqrt2 (z : ℂ) :
        invSqrt2 * (z * invSqrt2) = 2⁻¹ * z
        source
        @[simp]
        theorem QuantumAlg.PureState.star_invSqrt2 :
        star invSqrt2 = invSqrt2
        source
        @[simp]
        theorem QuantumAlg.PureState.norm_invSqrt2 :
        ‖invSqrt2‖ = (√2)⁻¹
        source
        theorem QuantumAlg.PureState.invSqrt2_ne_zero :
        invSqrt2 ≠ 0
        source
        noncomputable def QuantumAlg.PureState.ketPlusVec :
        StateVector 1

        Raw vector for the Hadamard-basis state |+⟩.

        Equations
        Instances For
          source
          noncomputable def QuantumAlg.PureState.ketMinusVec :
          StateVector 1

          Raw vector for the Hadamard-basis state |-⟩.

          Equations
          Instances For
            source
            @[simp]
            theorem QuantumAlg.PureState.ketPlusVec_apply (i : Fin (2 ^ 1)) :
            ketPlusVec.ofLp i = invSqrt2
            source
            @[simp]
            theorem QuantumAlg.PureState.ketMinusVec_apply (i : Fin (2 ^ 1)) :
            ketMinusVec.ofLp i = if i = 0 then invSqrt2 else -invSqrt2
            source
            theorem QuantumAlg.PureState.norm_sq_invSqrt2 :
            ‖invSqrt2‖ ^ 2 = 2⁻¹
            source
            theorem QuantumAlg.PureState.norm_eq_two_terms (psi : StateVector 1) :
            ‖psi‖ = √(‖psi.ofLp 0‖ ^ 2 + ‖psi.ofLp 1‖ ^ 2)

            Norm over Fin (2 ^ 1) as a two-term sum.

            source
            theorem QuantumAlg.PureState.norm_ketPlusVec :
            ‖ketPlusVec‖ = 1
            source
            theorem QuantumAlg.PureState.norm_ketMinusVec :
            ‖ketMinusVec‖ = 1
            source
            noncomputable def QuantumAlg.PureState.ketPlus :
            PureState 1

            |+> = (|0> + |1>)/sqrt 2.

            Equations
            Instances For
              source
              noncomputable def QuantumAlg.PureState.ketMinus :
              PureState 1

              |-> = (|0> - |1>)/sqrt 2.

              Equations
              Instances For
                source
                @[simp]
                theorem QuantumAlg.PureState.ketPlus_apply (i : Fin (2 ^ 1)) :
                ketPlus.vec.ofLp i = invSqrt2
                source
                @[simp]
                theorem QuantumAlg.PureState.ketMinus_apply (i : Fin (2 ^ 1)) :
                ketMinus.vec.ofLp i = if i = 0 then invSqrt2 else -invSqrt2
                source
                @[simp]
                theorem QuantumAlg.PureState.norm_ketPlus :
                ‖ketPlus‖ = 1
                source
                @[simp]
                theorem QuantumAlg.PureState.norm_ketMinus :
                ‖ketMinus‖ = 1
                source
                theorem QuantumAlg.PureState.probQubit0_ket0_tensor_add_ket1_tensor {n : ℕ} (alpha beta : StateVector n) :
                (ket0.vec.tensor alpha + ket1.vec.tensor beta).probQubit0 0 = ‖alpha‖ ^ 2

                Workhorse for test circuits: on |0> ⊗ alpha + |1> ⊗ beta the probability of reading 0 on qubit 0 is ‖alpha‖^2.

                source
                theorem QuantumAlg.PureState.probQubit1_ket0_tensor_add_ket1_tensor {n : ℕ} (alpha beta : StateVector n) :
                (ket0.vec.tensor alpha + ket1.vec.tensor beta).probQubit0 1 = ‖beta‖ ^ 2

                On |0> ⊗ alpha + |1> ⊗ beta the probability of reading 1 on qubit 0 is ‖beta‖^2.