Axioms for the theory of proveit.physics.quantum.QPE¶
In [1]:
import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit import Literal, ExprArray, ExprRange, ExprTuple
from proveit import a, b, c, d, e, eps, k, l, m, n, r, s, t, U
from proveit.logic import Equals, Forall, NotEquals, InSet, Set
from proveit.numbers import (zero, one, two, three, i, pi, Div, Exp, Abs,
Integer, Interval, IntervalCO, Natural, NaturalPos, Neg)
from proveit.numbers import (zero, one, two, three, i, pi, Div, Exp,
Integer, Interval, IntervalCO, IntervalOC, Natural, NaturalPos, Neg)
from proveit.numbers import (Add, exp, Ceil, Floor, frac, greater_eq, LessEq, Mod, ModAbs,
Mult, Prod, Round, subtract, Sum, Log, sqrt)
from proveit.linear_algebra import (
VecAdd, MatrixMult, ScalarMult, TensorExp, TensorProd, Norm)
from proveit.physics.quantum import (
Meas, NumBra, NumKet, RegisterU, Qmult,
QubitRegisterSpace, ket0, ket1)
#from proveit.physics.quantum.circuit import (Circuit, Input, Output, Gate, MultiQubitGate,
# IdentityOp, MultiWire, CircuitEquiv)
from proveit.physics.quantum.circuits import QcircuitEquiv
from proveit.physics.quantum.QPE import (
_eps, _alpha_m, _b, _b_round, _delta_b, _delta_b_round, _m_domain,
_n, _s, _t, _phase, _phase_est, _psi_t_ket, _psi__t_ket, _Psi_ket,
_two_pow_t, two_pow_t, _ket_u, _U, _U_pow_two_pow_k,
_QPE_U_t, _QPE1_U_t, _QPE_U_t_circuit, QPE1_U_t_circuit,
_psi_t_circuit, _Psi_circuit, _phase_est_circuit,
_Omega, _sample_space, _e_domain, _success_prob_e, _fail_prob_e)
from proveit.physics.quantum.QPE.phase_est_ops import ModAdd, Pfail, Psuccess, SubIndexed
from proveit.physics.quantum.QFT import InverseFourierTransform
from proveit.statistics import Prob
In [2]:
%begin axioms
Quantum circuit definitions¶
In [3]:
QPE1_def = Forall(
(s, t), Forall(
U, QcircuitEquiv(_QPE1_U_t.literals_as_variables(_U, _t, _s),
QPE1_U_t_circuit),
domain=RegisterU(s)),
domain=NaturalPos)
QPE1_def: 
In [4]:
QPE_def = Forall(
(s, t), Forall(
U, QcircuitEquiv(_QPE_U_t.literals_as_variables(_U, _t, _s),
_QPE_U_t_circuit.literals_as_variables(_U, _t, _s)),
domain=RegisterU(s)),
domain=NaturalPos)
QPE_def: 
Local axioms for convenience (i.e., used only within the QPE package)¶
Let $U$ be a unitary operator that acts on $s$ qubits, with $\lvert u\rangle$ as an eigenstate of $U$ with eigenvalue $e^{2 \pi i \varphi}$: $U \lvert u\rangle = e^{2 \pi i \varphi} \lvert u\rangle$.
In [5]:
# t (represented by the Literal t_)
# denotes the number of Qbits in the input register
_t_in_natural_pos = InSet(_t, NaturalPos)
_t_in_natural_pos: 
In [6]:
_s_in_nat_pos = InSet(_s, NaturalPos)
_s_in_nat_pos: 
In [7]:
_unitary_U = InSet(_U, RegisterU(_s))
_unitary_U: 
In [8]:
_u_ket_register = InSet(_ket_u, QubitRegisterSpace(_s))
_u_ket_register: 
In [9]:
_normalized_ket_u = Equals(Norm(_ket_u), one)
_normalized_ket_u: 
In [10]:
_phase_in_interval = InSet(_phase, IntervalCO(zero, one))
_phase_in_interval: 
In [11]:
_eigen_uu = Equals(MatrixMult(_U, _ket_u),
ScalarMult(exp(Mult(two, pi, i, _phase)), _ket_u))
_eigen_uu: 
In [12]:
_mod_add_def = Forall(
(a, b),
Equals(ModAdd(a, b), Mod(Add(a, b), _two_pow_t)),
domain=Integer)
_mod_add_def: 
In [13]:
_psi_t_def = Forall(
t, Equals(
_psi_t_ket,
TensorProd(ExprRange(r,
ScalarMult(frac(one, sqrt(two)),
VecAdd(ket0,
ScalarMult(exp(Mult(two, pi, i, Exp(two, r), _phase)),
ket1))),
subtract(t, one), zero, order='decreasing'))),
domain=NaturalPos)
_psi_t_def: 
In [14]:
_Psi_def = Equals(_Psi_ket, Qmult(InverseFourierTransform(_t),
_psi__t_ket))
_Psi_def: 
In [15]:
_sample_space_def = Equals(_Omega, _sample_space)
_sample_space_def: 
In [16]:
_alpha_m_def = Forall(
m,
Equals(_alpha_m,
Qmult(NumBra(m, _t),
_Psi_ket)),
domain=_m_domain)
_alpha_m_def: 
Let $\lvert \Psi \rangle$ be the outcome of the $t$-qubit register of ${\rm QPE}(U, t)$ acting on $\lvert u \rangle$, $m$ be a random variable representing the measurement of Psi with the register interpreted as an integer (via binary representation), and $\varphi_m = 2 \pi m/2^t$ be the random variable phase outcome of ${\rm QPE}(U, t)$:
Let $b_{f}$ be the value for $m$ that gives the closest $\varphi_m$ to $\varphi$ without exceeding it (the subscript $f$ stands for "floor"); similarly, let $b_{r}$ be the value for m that gives the closest $\varphi_m$ to $\varphi$ whether it be above or below the actual value (i.e., the subscript $r$ stands for "rounding"), and let $\delta_{b}$ be the difference between the actual value $\varphi$ and its estimate $b_f$ or $b_r$:
In [17]:
from proveit.physics.quantum.QPE import _b_floor
_best_floor_def = Equals(_b_floor, Floor(Mult(_two_pow_t, _phase)))
_best_floor_def: 
In [18]:
_best_round_def = Equals(_b_round, Round(Mult(_two_pow_t, _phase)))
_best_round_def: 
In [19]:
_delta_b_def = Forall(
b,
Equals(_delta_b, subtract(_phase, frac(b, _two_pow_t))),
domain = Integer)
_delta_b_def: 
The probability of success is defined as $\theta_m$ being within some epsilon of $\theta$:
In [20]:
_success_def = Forall(
e,
Equals(Psuccess(e),
_success_prob_e),
domain=_e_domain).with_wrapping()
_success_def: 
In [21]:
_fail_def = Forall(
e,
Equals(Pfail(e), _fail_prob_e),
domain=_e_domain).with_wrapping()
_fail_def: 
Let $\alpha_l$ be the amplitude of $\lvert \Psi \rangle$ for the $b \oplus l$ state, where $\oplus$ is defined as addition modulo $2^t$:
In [22]:
# n (represented by the Literal _n)
# denotes the desired bits of precision (and thus n ≤ t)
_n_in_natural_pos = InSet(_n, NaturalPos)
_n_in_natural_pos: 
In [23]:
# n (represented by the Literal _n)
# denotes the desired bits of precision (and thus n ≤ t)
# n ≥ 2 helps with some details in some of the final steps of
# the overall general theorem, but the assumption should be revisited later
_n_ge_two = greater_eq(_n, two)
_n_ge_two: 
In [24]:
_eps_in_interval = InSet(_eps, IntervalOC(zero, one))
_eps_in_interval: 
In [25]:
_t_req = greater_eq(
_t, Add(_n, Ceil(Log(two, Add(two, frac(one, Mult(two, _eps)))))))
_t_req: 
In [26]:
%end axioms