Foundations of Quantum Programming

6.9 Proofs of lemmas, propositions and theorems

The proofs of the main lemmas, propositions and theorems in this chapter all include tedious calculations. So, for readability, these results have been stated in the previous sections without proofs. To complete this chapter, here we present their detailed proofs.

Proof of Lemma 6.3.2. Let F be the operator-valued function given in Definition 6.3.5. We write:

$\begin{array}{l}\hfill \overline{F}\stackrel{△}{=}\sum _{{\delta }_1\in {\mathrm{\Delta }}_1,\dots ,{\delta }_n\in {\mathrm{\Delta }}_n}F{({\oplus }_{i=1}^n{\delta }_i)}^{†}\cdot F({\oplus }_{i=1}^n{\delta }_i).\end{array}$

Let us start with an auxiliary equality. For any $|\mathrm{\Phi }\rangle ,|\mathrm{\Psi }\rangle \in {\mathcal{H}}_c\otimes \mathcal{H}$, we can write

$\begin{array}{l}\hfill |\mathrm{\Phi }\rangle =\sum _{i=1}^n|i\rangle |{\phi }_i\rangle \text{and ...}\end{array}$