Proof of Theorem 3.2, p.15, [23] — families with equal inner products are related by a unitary

Let $\mathcal H$ be a finite-dimensional complex Hilbert space and $\{v_a\}_{a\in\beta}$, $\{w_a\}_{a\in\beta}$ two families of vectors of $\mathcal H$ indexed by the same arbitrary set $\beta$, with identical inner-product relationships:

Then there is a unitary operator $U$ on $\mathcal H$ with $Uv_a=w_a$ for every $a$.

In the proof of Theorem 3.2 Knill and Laflamme apply this (citing [23]) to $v_a=A_a|0_L\rangle$ and $w_a=A_a|i_L\rangle$, whose inner products agree by condition (19), to obtain the unitaries $U_i$ with $U_iA_a|0_L\rangle=A_a|i_L\rangle$.

Differences from the source:

• encoding: an $n$-dimensional Hilbert space $\mathcal H$ and linear operators on it → EuclideanSpace ℂ ι for a finite type ι, operators Matrix ι ι ℂ acting by QAlgorithms.act; reason: Lean convention; every $n$-dimensional Hilbert space is isometric to $\mathbb C^n$, so the instances are the same
• generalization: unitaries $U_i$ with $U_iA_a|0_L\rangle=A_a|i_L\rangle$ for all $A_a$, from the identical inner-product relationships between the $A_a|0_L\rangle$ and the $A_a|i_L\rangle$ [23] → any two families v w : β → H with equal inner products are related by a unitary U ∈ Matrix.unitaryGroup ι ℂ; reason: this is the general fact the paper cites from [23]; taking $v_a=A_a|0_L\rangle$, $w_a=A_a|i_L\rangle$ gives the paper's claim