OAI/InformationTheory/QuantumCircuit/Physical.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.QAC.singleLocal line 13

   Source documentation

   A physical one-qubit gate, as a local layer.

   def singleLocal {N : ℕ} (q : Fin N) (u : Matrix.unitaryGroup Bit ℂ) : LocalLayer N :=
   …

   Mentions: OAI.QAC.Bit, OAI.QAC.LocalLayer

2. lemma OAI.QAC.local_gate_matrix line 16
3. lemma OAI.QAC.reflectList_rotate line 26
4. lemma OAI.QAC.reflectList_rotate_commute line 38
5. def OAI.QAC.normalCounts line 45

   Source documentation

   Local gates are moved to the right by rotating the product axes; supports are unchanged, so a disjoint physical layer yields one reflection layer.

   def normalCounts {N : ℕ} : List (Gate N) → List (Count N)
     | [] => []
     | .local q u :: l => (normalCounts l).map (fun A => A.rotate (singleLocal q u))
     | .toffoli c t _ :: l => toffoliCount c t :: normalCounts l

   Mentions: OAI.QAC.Gate, OAI.QAC.Count, OAI.QAC.singleLocal, OAI.QAC.toffoliCount

6. def OAI.QAC.normalLocal line 50
7. lemma OAI.QAC.normalCounts_support line 55
8. lemma OAI.QAC.normalCounts_disjoint line 73
9. lemma OAI.QAC.gateList_normal line 93
10. lemma OAI.QAC.physicalLayer_isCircuit line 107
11. lemma OAI.QAC.physicalCircuit_isCircuit line 115
12. lemma OAI.QAC.IsCircuit.succ line 124
13. lemma OAI.QAC.IsCircuit.mono line 128
14. lemma OAI.QAC.IsCircuit.local_mul line 134