OAI/InformationTheory/QuantumCircuit/Circuit.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.QAC.coe_sum_normSq line 11
2. lemma OAI.QAC.normalized_mulVec line 16
3. lemma OAI.QAC.rankOne_mulVec line 25
4. def OAI.QAC.orthogonalVector line 33

   Source documentation

   The canonical orthogonal unit vector in a qubit.

   def orthogonalVector (v : Bit → ℂ) : Bit → ℂ := ![-star (v 1), star (v 0)]

   Mentions: OAI.QAC.Bit

5. lemma OAI.QAC.orthogonalVector_normalized line 35
6. lemma OAI.QAC.rankOne_orthogonalVector line 39
7. def OAI.QAC.Count.rotate line 51

   Source documentation

   Conjugation by a local layer preserves the exact count support.

   def Count.rotate {N : ℕ} (M : Count N) (L : LocalLayer N) : Count N where
   …

   Mentions: OAI.QAC.Count, OAI.QAC.LocalLayer

8. lemma OAI.QAC.Count.rotate_zero line 56
9. def OAI.QAC.Count.flip line 69

   Source documentation

   Flipping any subset of the reference axes is still a count, not an added gate.

   def Count.flip {N : ℕ} (M : Count N) (F : Finset (Fin N)) : Count N where
   …

   Mentions: OAI.QAC.Count

10. lemma OAI.QAC.Count.flip_zero line 77
11. lemma OAI.QAC.localMatrix_unitary line 88
12. lemma OAI.QAC.localMatrix_mul line 91
13. lemma OAI.QAC.localMatrix_star line 95
14. lemma OAI.QAC.reflection_unitary line 99
15. lemma OAI.QAC.reflectionMatrix_unitary line 106
16. lemma OAI.QAC.IsCircuit.mem_unitary line 113
17. lemma OAI.QAC.IsCircuit.mul_local line 123
18. lemma OAI.QAC.IsCircuit.mul line 133
19. lemma OAI.QAC.star_list_prod_reverse line 143
20. def OAI.QAC.ReflectionLayer.reverse line 150
21. lemma OAI.QAC.reflectionMatrix_star line 154
22. lemma OAI.QAC.IsCircuit.star_mem line 160