Signal transformation ยท Primitives
Linear combination of unitaries
Theorem statement
Suppose $\{U_k\}_{k=0}^{2^m-1}$ is a set of $n$-qubit unitaries and $A=\sum_{k=0}^{2^m-1}c_kU_k$ for positive coefficients $c_k$. Let $U=\sum_{k=0}^{2^m-1}\ket{k}\!\bra{k}\otimes U_k$, and let $V$ be an $m$-qubit unitary such that $V\ket{0}=\|c\|_1^{-1/2}\sum_{k=0}^{2^m-1}\sqrt{c_k}\ket{k}$. Then $W=(V^\dagger\otimes I^{\otimes n})U(V\otimes I^{\otimes n})$ satisfies
$$
(\bra{0^{m}}\otimes I^{\otimes n})W(\ket{0^{m}}\otimes I^{\otimes n})
=
\|c\|_1^{-1}A.
$$
Sources
Lean context
- Import
QuantumAlg.Primitives.LCU- Lean declaration
QuantumAlg.LinearCombinationOfUnitaries.main
Copy a short prompt with the import, theorem name, citations, and public source link.