OAI/InformationTheory/QuantumCircuit/Toffoli.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.QAC.basisVector line 12

   Source documentation

   Computational basis vectors and the normalized minus vector.

   def basisVector (b : Bit) : Bit → ℂ := fun x => if x=b then 1 else 0

   Mentions: OAI.QAC.Bit

2. def OAI.QAC.halfScale line 14
3. lemma OAI.QAC.halfScale_sq line 16
4. lemma OAI.QAC.halfScale_nonneg line 20
5. lemma OAI.QAC.basisVector_normalized line 22
6. lemma OAI.QAC.rankOne_basis line 26
7. def OAI.QAC.minusVector line 32
8. lemma OAI.QAC.minusVector_normalized line 34
9. lemma OAI.QAC.rankOne_minus line 38
10. def OAI.QAC.toffoliCount line 44

    Source documentation

    The product projection in the exact Toffoli identity I-2 C⊗|-><-|.

    def toffoliCount {N : ℕ} (c : Finset (Fin N)) (t : Fin N) : Count N where
    …

    Mentions: OAI.QAC.Count

11. lemma OAI.QAC.toffoliCount_entry line 52
12. lemma OAI.QAC.toffoli_reflection line 88