# 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, ExprTuple
from proveit import a, b, eps, k, l, n, t
from proveit.linalg import MatrixProd, ScalarProd, TensorExp, TensorProd
from proveit.logic import Equals, Forall, InSet, Set
from proveit.numbers import zero, one, two, three, e, i, pi, Div, Exp, Integer, Interval, IntervalCO, NaturalPos
from proveit.numbers import Add, Exp, Floor, frac, LessEq, Mod, ModAbs, Mult, Prod, subtract, Sum
from proveit.physics.quantum import (Ket, Meas, RegisterBra, RegisterSU,
QubitRegisterSpace, ket0, ket1, Hgate, CONTROL, SPACE)
from proveit.physics.quantum.circuit import Circuit, Input, Output, MultiQubitGate, IdentityOp
from proveit.physics.quantum.QPE import (alpha_l, b_, delta_, m_, n_, phase_, psi_,
phase_m_, psi_k, psi_1, Psi_, psi_next, t_, two_pow_t,
u_, U_, U_pow_two_pow_k, p_0, p_k )
from proveit.physics.quantum.QPE.phase_est_ops import ModAdd, Pfail, Psuccess, SubIndexed
from proveit.statistics import Prob

In [2]:
%begin axioms

Defining axioms for theory 'proveit.physics.quantum.QPE'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions


Let $U$ be a unitary operator that acts on $n$ qubits, with $\lvert u\rangle$ as an eigenstate of $U$ with eigenvalue $e^{2 \pi i \varphi}$:

In [3]:
n_in_nat_pos = InSet(n_, NaturalPos)

Out[3]:
n_in_nat_pos:
In [4]:
unitary_u = InSet(U_, RegisterSU(n_))

Out[4]:
unitary_u:
In [5]:
u_ket_register = InSet(Ket(u_), QubitRegisterSpace(n_))

Out[5]:
u_ket_register:
In [6]:
phase_in_interval = InSet(phase_, IntervalCO(zero, one))

Out[6]:
phase_in_interval:
In [7]:
eigen_uu = Equals(MatrixProd(U_, Ket(u_)), ScalarProd(Exp(e, Mult(two, pi, i, phase_)), Ket(u_)))

Out[7]:
eigen_uu:
In [8]:
# t (represented by the Literal t_)
# denotes the number of Qbits in the input register
t_in_natural_pos = InSet(t_, NaturalPos)

Out[8]:
t_in_natural_pos:
In [9]:
psi_kets_in_q_reg_space = Forall(k, InSet(Ket(psi_k), QubitRegisterSpace(k)), domain=NaturalPos)

Out[9]:
psi_kets_in_q_reg_space:
In [10]:
PsiKetInQRegSpace = InSet(Ket(Psi_), QubitRegisterSpace(t_))

Out[10]:
PsiKetInQRegSpace:
In [11]:
p_k_def = Forall(
k,
Equals(
p_k,
Mult(frac(one, Exp(two, frac(one,two))),
Add(ket0, Mult( Exp(e, Mult(two, pi, i, phase_, Exp(two, k))), ket1)))),
domain=Interval(zero, subtract(t_, one)))

Out[11]:
p_k_def:
In [12]:
psi_1_equals_p_0 = Equals(psi_1, p_0)

Out[12]:
psi_1_equals_p_0:
In [13]:
psi_k_def = Forall(
k,
Equals(
TensorProd(p_k, SubIndexed(psi_, k))),
domain=Interval(one, subtract(t_, one)))

Out[13]:
psi_k_def:
In [14]:
first_q_p_e = Circuit(ExprArray(ExprTuple(Input(ket0), Hgate, MultiQubitGate(CONTROL, Set(one, two)), Output(Ket(psi_1))),
ExprTuple(Input(Ket(u_)), IdentityOp(), MultiQubitGate(U_, Set(one, two)), Output(Ket(u_)))))

Out[14]:
first_q_p_e:
In [15]:
# mid_q_p_e = Forall(k,
#                Circuit([[Input(Ket(psi_k)), MultiWire(k), PASS, WIRE_DN, PASS, PASS],
#                 [Input(Ket(u_)), MultiWire(n_), Gate(U_pow_two_pow_k), Output(Ket(u_)), PASS, PASS]]),
#        domain=NaturalPos)

In [16]:
# Working to translate/update to use current Circuit params
mid_q_p_e = Forall(k,
Circuit(ExprArray(
ExprTuple(Input(Ket(psi_k)), IdentityOp(), IdentityOp(), MultiQubitGate(IdentityOp(), Set(one, two)), SPACE, SPACE),
ExprTuple(Input(ket0), Hgate, MultiQubitGate(CONTROL, Set(two, three)), MultiQubitGate(IdentityOp(), Set(one, two)), IdentityOp(), Output(Ket(psi_next))),
ExprTuple(Input(Ket(u_)), IdentityOp(), MultiQubitGate(U_pow_two_pow_k, Set(two, three)), Output(Ket(u_)), SPACE, SPACE))),
domain=NaturalPos)

Out[16]:
mid_q_p_e:
In [17]:
# final_q_p_e = Circuit([[Input(Ket(psi_t)), MultiWire(t_), Gate(InverseFourierTransform(t_)), Output(Ket(Psi_))]])

In [18]:
# trying here to define Psi_1 (the result at the end of "stage 1")
# represented in Nielsen & Chuang's Eq 5.20 (pg 222)
Psi_1 = Literal(string_format='Psi_1', latex_format=r'\Psi_{1}')
phi_ = Literal(string_format='phi', latex_format=r'\varphi')
Psi_1_def = Equals(Psi_1,
Mult(frac(one, Exp(two, frac(t_,two))),
Sum(k, Mult(Exp(e, Mult(two, pi, i, phase_, k)), Ket(k)), domain=Interval(zero, subtract(Exp(two, t_), one)))))

Out[18]:
Psi_1_def:
In [ ]:



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 interpretted 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)$:

In [19]:
m_def = Equals(m_, Meas(Ket(Psi_)))

Out[19]:
m_def:
In [20]:
phase_m_def = Equals(phase_m_, frac(m_, two_pow_t))

Out[20]:
phase_m_def:

Let $b$ be the value for $m$ that gives the closest $\varphi_m$ to $\varphi$ without exceeding it, and let $\delta$ be this difference:

In [21]:
best_def = Equals(b_, Floor(Mult(phase_, two_pow_t)))

Out[21]:
best_def:
In [22]:
delta_def = Equals(delta_, subtract(phase_, frac(b_, two_pow_t)))

Out[22]:
delta_def:

The probability of success is defined as $\theta_m$ being within some epsilon of $\theta$:

In [23]:
success_def = Forall(
eps,
Equals(Psuccess(eps),
Prob(LessEq(ModAbs(subtract(m_, b_), two_pow_t), eps), m_)),
domain=NaturalPos)

Out[23]:
success_def:
In [24]:
fail_def = Forall(
eps,
Equals(Pfail(eps), subtract(one, Psuccess(eps))),
domain=NaturalPos)

Out[24]:
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 [25]:
mod_add_def = Forall(
(a, b),
domain=Integer)

Out[25]:
In [26]:
alpha_def = Forall(
l,
Equals(alpha_l,

%end axioms

These axioms may now be imported from the theory package: proveit.physics.quantum.QPE