In this package, we prove outcome bounds for the Quantum Phase Estimation algorithm. Our proof is based on the proof in pp. 221--225 of Michael A. Nielsen and Isaac L. Chuang, "Quantum Computation and Quantum Information", (10th Anniversary Edition). Cambridge University Press, New York, NY, 2010.
import proveit
%theory # toggles between interactive and static modes