OAI/InformationTheory/QuantumCircuit/ParityTrace.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.QAC.bitSign_add line 11
2. lemma OAI.QAC.bitSign_finset_sum line 14
3. lemma OAI.QAC.bitSign_parity line 21
4. lemma OAI.QAC.sum_bitSign_parity line 24
5. def OAI.QAC.inputSign line 29
6. lemma OAI.QAC.inputPhase_diagonal line 32
7. lemma OAI.QAC.inputSign_inputWord line 43
8. lemma OAI.QAC.trace_phase_ancilla line 60
9. lemma OAI.QAC.parity_trace_identity line 71

   Source documentation

   Character orthogonality as a finite-dimensional cyclic trace identity.

   lemma parity_trace_identity {n N : ℕ} (hnN : n ≤ N) (B : Operator N) :
       (∑ x : Word n, (localMatrix (inputHadamard n N)*B*localMatrix (inputHadamard n N))
         (flipWord (inputSet n N) (inputWord x)) (inputWord x)) =
       ∑ x : Word n, (bitSign (parity x):ℂ)*B (inputWord x) (inputWord x) := by
   …

   Mentions: OAI.QAC.Operator, OAI.QAC.Word, OAI.QAC.localMatrix, OAI.QAC.inputHadamard, OAI.QAC.flipWord, OAI.QAC.inputSet, OAI.QAC.inputWord, OAI.QAC.bitSign, OAI.QAC.parity