OAI/Computability/QuantumFactoring/RegisterCircuit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ExactQuantumFactoring.Register line 14

   Source documentation

   A physical placement of a register uses distinct existing qubits.

   abbrev Register (p q : ℕ) := Fin p ↪ Fin q
   …

2. abbrev OAI.ExactQuantumFactoring.Register.Unused line 18
3. def OAI.ExactQuantumFactoring.Register.split line 20
4. def OAI.ExactQuantumFactoring.Register.liftMatrix line 41
5. lemma OAI.ExactQuantumFactoring.Register.liftMatrix_one line 46
6. lemma OAI.ExactQuantumFactoring.Register.liftMatrix_mul line 51
7. lemma OAI.ExactQuantumFactoring.Register.liftMatrix_unitary line 63
8. def OAI.ExactQuantumFactoring.Instruction.place line 70
9. lemma OAI.ExactQuantumFactoring.Instruction.place_matrix line 73
10. lemma OAI.ExactQuantumFactoring.programMatrix_place line 104
11. def OAI.ExactQuantumFactoring.Register.pairState line 113

    Source documentation

    Tensor states in the actual physical wire order.

    noncomputable def Register.pairState {p q : ℕ} (w : Register p q)
        (v : State p) (z : (w.Unused → Bool) → ℂ) : State q :=
    …

    Mentions: OAI.ExactQuantumFactoring.Register, OAI.ExactQuantumFactoring.State

12. lemma OAI.ExactQuantumFactoring.Register.liftMatrix_pairState line 117