OAI/InformationTheory/QuantumCircuit/Computational.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.QAC.matrix_entry_norm_le line 12
2. lemma OAI.QAC.tensorMatrix_diagonal line 23
3. lemma OAI.QAC.rankOne_basis_diagonal line 34
4. lemma OAI.QAC.one_sub_rankOne_basis line 40
5. def OAI.QAC.computationalCount line 47

   Source documentation

   A full computational-basis count.

   def computationalCount {N : ℕ} (z : Word N) : Count N where
   …

   Mentions: OAI.QAC.Word, OAI.QAC.Count

6. def OAI.QAC.basisProjection line 52
7. lemma OAI.QAC.computationalCount_zero line 55
8. def OAI.QAC.flipWord line 66

   Source documentation

   Complement selected computational bits.

   def flipWord {N : ℕ} (F : Finset (Fin N)) (z : Word N) : Word N :=
   …

   Mentions: OAI.QAC.Word

9. lemma OAI.QAC.flipWord_involutive line 69
10. lemma OAI.QAC.computationalCount_pattern line 78
11. lemma OAI.QAC.basisProjection_mul_entry line 90
12. lemma OAI.QAC.mul_basisProjection_entry line 95
13. lemma OAI.QAC.high_entry_bound line 100
14. def OAI.QAC.inputSet line 120

    Source documentation

    Input positions; ancillas occupy the other positions.

    def inputSet (n N : ℕ) : Finset (Fin N) := Finset.univ.filter (fun i => i.val<n)

15. lemma OAI.QAC.inputSet_card line 122
16. def OAI.QAC.bitSign line 126

    Source documentation

    The real character of a single bit.

    def bitSign (b : Bit) : ℝ := if b=0 then 1 else -1

    Mentions: OAI.QAC.Bit

17. def OAI.QAC.bitX line 128
18. def OAI.QAC.bitZ line 129
19. def OAI.QAC.bitH line 130
20. lemma OAI.QAC.halfScale_complex_sq line 132
21. lemma OAI.QAC.bitH_star line 136
22. lemma OAI.QAC.bitH_sq line 140
23. lemma OAI.QAC.bitH_unitary line 146
24. def OAI.QAC.hadamardGate line 149
25. lemma OAI.QAC.bitH_X_H line 151
26. def OAI.QAC.inputHadamard line 157
27. def OAI.QAC.inputFlip line 159
28. def OAI.QAC.inputPhase line 160
29. lemma OAI.QAC.inputHadamard_star line 162
30. lemma OAI.QAC.inputHadamard_flip line 173