OAI/InformationTheory/QuantumCircuit/Ancilla.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.QAC.ancillaValid line 12

   Source documentation

   The zero-ancilla computational subspace, without any condition on final garbage.

   def ancillaValid {N : ℕ} (n : ℕ) (z : Word N) : Prop := ∀ i, n ≤ i.val → z i=0

   Mentions: OAI.QAC.Word

2. instance OAI.QAC.(instance at line 14) line 14
3. def OAI.QAC.restrictWord line 18
4. lemma OAI.QAC.restrict_inputWord line 21
5. lemma OAI.QAC.inputWord_injective line 26
6. lemma OAI.QAC.inputWord_valid line 30
7. lemma OAI.QAC.input_restrictWord line 34
8. lemma OAI.QAC.sum_ancillaValid line 41
9. def OAI.QAC.ancillaProjection line 59
10. lemma OAI.QAC.ancillaProjection_diagonal line 62
11. lemma OAI.QAC.inputHadamard_ancilla_flip line 83
12. lemma OAI.QAC.bitX_entry line 94
13. lemma OAI.QAC.inputFlip_entry line 97
14. lemma OAI.QAC.ancillaValid_flip line 109
15. lemma OAI.QAC.inputFlip_mul_ancilla_entry line 117
16. lemma OAI.QAC.trace_flip_ancilla line 131