OAI/Computability/QuantumFactoring/GateSemantics.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ExactQuantumFactoring.sum_boolFin_succ line 12
  2. lemma OAI.ExactQuantumFactoring.sum_boolFin_zero line 21
  3. def OAI.ExactQuantumFactoring.Primitive.localMatrix line 25
  4. def OAI.ExactQuantumFactoring.permutationMatrix line 30

    Source documentation

    A reversible Boolean operation, viewed as an exact permutation matrix.

    noncomputable def permutationMatrix {ι : Type*} [DecidableEq ι] (e : Equiv.Perm ι) :
    Matrix ι ι ℂ := Matrix.of (fun a b => if a = e b then 1 else 0)
  5. lemma OAI.ExactQuantumFactoring.permutationMatrix_unitary line 33
  6. def OAI.ExactQuantumFactoring.notPerm line 41
  7. def OAI.ExactQuantumFactoring.cnotPerm line 47
  8. def OAI.ExactQuantumFactoring.toffoliPerm line 53
  9. lemma OAI.ExactQuantumFactoring.not_localMatrix line 59
  10. lemma OAI.ExactQuantumFactoring.cnot_localMatrix line 66
  11. lemma OAI.ExactQuantumFactoring.toffoli_localMatrix line 73
  12. lemma OAI.ExactQuantumFactoring.hadamard_local_unitary line 80
  13. lemma OAI.ExactQuantumFactoring.phase_local_unitary line 100
  14. lemma OAI.ExactQuantumFactoring.Primitive.local_unitary line 115
  15. lemma OAI.ExactQuantumFactoring.unitary_reindex line 124
  16. def OAI.ExactQuantumFactoring.controlledMatrix line 135
  17. lemma OAI.ExactQuantumFactoring.controlledMatrix_unitary line 141
  18. def OAI.ExactQuantumFactoring.Gate.baseLocalMatrix line 156
  19. lemma OAI.ExactQuantumFactoring.Gate.baseLocalMatrix_eq line 160
  20. lemma OAI.ExactQuantumFactoring.Gate.baseLocal_unitary line 166
  21. def OAI.ExactQuantumFactoring.Gate.localMatrix line 173
  22. lemma OAI.ExactQuantumFactoring.Gate.controlled_localMatrix line 176
  23. lemma OAI.ExactQuantumFactoring.Gate.local_unitary line 189