Common expressions for the theory of proveit.physics.quantum.QPE¶
In [1]:
import proveit
%common_expressions_notebook # Keep this at the top following 'import proveit'.
from proveit import defaults
from proveit import (Literal, Variable, ExprRange, ExprArray, VertExprArray,
ConditionalSet, Conditional)
from proveit import a, b, e, i, j, k, l, m, n, r, s, t, u, U, eps
from proveit.logic import (Set, Difference, InSet, Set, CartExp,
Equals, NotEquals, SetOfAll)
from proveit.numbers import (
zero, one, two, Abs, Add, Ceil, Complex, Exp, frac, greater, greater_eq,
Interval, LessEq, Log, ModAbs, NaturalPos, Neg, Mult, Round, subtract, subtract)
from proveit.linear_algebra import MatrixExp
from proveit.statistics import Prob, ProbOfAll
from proveit.physics.quantum import Ket, NumKet, MEAS, I, Z, H, CONTROL, ket_plus
from proveit.physics.quantum.circuits import (
Qcircuit, Input, Output, Gate, Measure, control_elem, multi_wire,
multi_input_entries, multi_output_entries, multi_gate_entries,
multi_measure_entries)
from proveit.physics.quantum.QFT import InverseFourierTransform
from proveit.physics.quantum.QPE import QPE, QPE1
from proveit.physics.quantum.QPE.phase_est_ops import ModAdd, SubIndexed
from proveit.numbers import Round
In [2]:
%begin common
In [3]:
# U: Unitary operator to apply quantum phase estimation.
_U = Literal('U')
_U: 
In [4]:
# n: Number of qubits which U acts on.
_n = Literal('n')
_n: 
In [5]:
# u: Eigenvector of U to apply the quantum phase estimation.
_ket_u = Literal('|u>', r'\lvert u \rangle')
_ket_u: 
In [6]:
# phase: Eigenvalue phase of u w.r.t. U. U u = e^{i \varphi} u.
# This \varphi is the phase that is the objective of phase estimation.
_phase = Literal('phase', latex_format=r'\varphi')
_phase: 
In [7]:
_phase_est = Literal('phase_est', latex_format=r'\tilde{\varphi}')
_phase_est: 
In [8]:
phase = Variable('phase', latex_format=r'\varphi')
phase:
In [9]:
phase_est = Variable('phase_est', latex_format=r'\tilde{\varphi}')
phase_est:
In [10]:
# t: Number of qubit registers for the quantum phase estimation.
# We prove that this is the bits of precision of phase estimation.
_t = Literal('t')
_t: 
In [11]:
_n = Literal('n')
_n:
In [12]:
_eps = Literal('eps', r'\epsilon')
_eps: 
In [13]:
# Psi: Outcome of register qubits following the quantum phase estimation circuit.
_Psi_ket = Literal('|Psi>', latex_format=r'\lvert \Psi \rangle')
_Psi_ket: 
In [14]:
# psi: indexed intermediate output registers inside the quantum phase estimation circuit.
_psi = Literal('psi', latex_format=r'\psi')
_psi: 
In [15]:
# SubIndexed puts in in a ket for display purposes.
_psi_t_ket = SubIndexed(_psi, t)
_psi_t_ket: 
In [16]:
_psi__t_ket = SubIndexed(_psi, _t)
_psi__t_ket:
In [17]:
_psi_1 = SubIndexed(_psi, one)
_psi_1: 
In [18]:
_U_pow_two_pow_k = Exp(_U, Exp(two, k))
_U_pow_two_pow_k: 
In [19]:
_s = Literal('s')
_s: 
In [20]:
# Used to be
# m: Random variable for the measurement of Psi as an
# integer from the register's binary representation.
# Now we are using it as the size of the |u> register.
# As of 10/25 back to using this for the measurement of Psi
# Now using s as the size of the |u> register
#_m = Literal('m')
In [21]:
# phase_m: Random variable for the phase result of the
# quantum phase estimation phase_m = m / 2^t
# (I wish the subscript appeared a bit lower)
#_phase_m = Literal('phase_m', latex_format=r'\varphi_m')
In [22]:
# b: The "best" outcome of measurement m, defined in Nielsen & Chuang
# such that b is the t-qubit estimate closest to, BUT LESS THAN, phase phi.
_b = Literal('b')
_b: 
In [23]:
# b_f: The "best" outcome of measurement m, defined (in the axioms) as
# the best t-qubit under-estimate of the phase phi (i.e. the binary expansion
# of phi truncated to t-bits). The 'f' stands for 'floor'.
_b_floor = Literal('b_{f}', latex_format=r'b_{\textit{f}}')
_b_floor: 
In [24]:
# b_r: The "best" outcome of measurement m, now defined (in the axioms) as
# the t-qubit estimate closest to phase phi (i.e. the binary expansion of
# phi ROUNDED to t-bits). The 'r' stands for 'round'.
_b_round = Literal('b_{r}', latex_format=r'b_{\textit{r}}')
_b_round: 
In [25]:
two_pow_t = Exp(two, t)
two_pow_t: 
In [26]:
two_pow_s = Exp(two, s)
two_pow_s: 
In [27]:
# 2^t
_two_pow_t = Exp(two, _t)
_two_pow_t:
In [28]:
# 2^{t-1}
_two_pow__t_minus_one = Exp(two, subtract(_t, one))
_two_pow__t_minus_one: 
In [29]:
# 2^{t+1}
_two_pow__t_plus_one = Exp(two, Add(_t, one))
_two_pow__t_plus_one: 
In [30]:
_two_pow_t__minus_one = subtract(Exp(two, _t), one)
_two_pow_t__minus_one: 
In [31]:
# amplitude of output register as indexed
_alpha = Literal('alpha', latex_format= r'\alpha')
_alpha: 
In [32]:
# These are subscripted with letter l (ell), NOT numeral 1 (one)
_alpha_l = SubIndexed(_alpha, l)
_alpha_l: 
In [33]:
_alpha_m = SubIndexed(_alpha, m)
_alpha_m: 
In [34]:
from proveit.numbers import Mod
_alpha_l_mod_two_pow_t = SubIndexed(_alpha, Mod(l, _two_pow_t))
_alpha_l_mod_two_pow_t: 
In [35]:
from proveit import m
from proveit.numbers import Mod
_alpha_m_mod_two_pow_t = SubIndexed(_alpha, Mod(m, _two_pow_t))
_alpha_m_mod_two_pow_t: 
In [36]:
# These are subscripted with letter l (ell), NOT numeral 1 (one)
_alpha_bl = SubIndexed(_alpha, ModAdd(_b, l))
_alpha_bl: 
In [37]:
abs_a = Abs(a)
abs_a: 
In [38]:
_abs_alpha_l = Abs(_alpha_l)
_abs_alpha_l: 
In [39]:
_alpha_l_sqrd = Exp(Abs(_alpha_l), two)
_alpha_l_sqrd: 
In [40]:
_rel_indexed_alpha = SubIndexed(_alpha, ModAdd(_b_floor, l))
_rel_indexed_alpha: 
In [41]:
_alpha_m_sqrd = Exp(Abs(_alpha_m), two)
_alpha_m_sqrd: 
In [42]:
# _delta: difference between the phase and the best t-qubit
# phase phase measurement _b/2^t (defined in axioms)
_delta = Literal('delta', latex_format=r'\delta')
_delta: 
In [43]:
_delta_b = SubIndexed(_delta, b)
_delta_b: 
In [44]:
# _delta__b_floor: difference between the phase and the best
# t-qubit phase underestimate measurement _b_round/2^t (defined in axioms)
# _delta_b_floor = Literal('delta_{b_f}', latex_format=r'\delta_{b_f}')
In [45]:
# _delta__b_floor: difference between the phase and the best
# t-qubit phase underestimate measurement _b_round/2^t (defined in axioms)
_delta_b_floor = SubIndexed(_delta, _b_floor)
_delta_b_floor: 
In [46]:
# _delta_round: difference between the phase and the best (rounded)
# t-qubit phase phase measurement _b_round/2^t (defined in axioms)
_delta_b_round = SubIndexed(_delta, _b_round)
_delta_b_round: 
In [47]:
_diff_l_scaled_delta_floor = subtract(l, Mult(_two_pow_t, _delta_b_floor))
_diff_l_scaled_delta_floor: 
In [48]:
_full_domain = Interval(Add(Neg(Exp(two, subtract(_t, one))), one),
Exp(two, subtract(_t, one)))
_full_domain: 
In [49]:
_neg_domain = Interval(Add(Neg(_two_pow__t_minus_one), one),
Neg(Add(e, one)))
_neg_domain: 
In [50]:
_pos_domain = Interval(Add(e, one),
_two_pow__t_minus_one)
_pos_domain: 
In [51]:
_e_domain = Interval(one, subtract(_two_pow__t_minus_one, two))
_e_domain: 
In [52]:
_e_value = subtract(Exp(two, subtract(_t, _n)), one)
_e_value: 
In [53]:
s_ket_domain = CartExp(Complex, Exp(two, s))
s_ket_domain: 
In [54]:
_t_wire = multi_wire(_t)
_s_wire = multi_wire(_s)
_s_wire: 
In [55]:
_qpe_multigate = [*multi_gate_entries(
QPE(_U, _t), one, Add(_t, _s), (one, _t), (Add(_t, one), Add(_t, _s)))]
_QPE_U_t = Qcircuit(VertExprArray(
_qpe_multigate))
_QPE_U_t: 
In [56]:
_qpe1_multigate = [*multi_gate_entries(
QPE1(_U, _t), one, Add(_t, _s), (one, _t), (Add(_t, one), Add(_t, _s)))]
_QPE1_U_t = Qcircuit(VertExprArray(
_qpe1_multigate))
_QPE1_U_t: 
In [57]:
_inv_FT = [*multi_gate_entries(InverseFourierTransform(_t), one, _t, (one, _t))]
_QPE_U_t_circuit = Qcircuit(VertExprArray(
_qpe1_multigate, [*_inv_FT, _s_wire]))
_QPE_U_t_circuit: 
These assumptions are needed for proper formatting of QPE1_U_t_circuit.
In [58]:
_qpe_inputs = [ExprRange(i, Input(ket_plus), one, _t),
*multi_input_entries(_ket_u, Add(_t, one), Add(_t, _s), (one, _s))]
_u_outputs = [*multi_output_entries(_ket_u, Add(_t, one), Add(_t, _s),
(one, _s))]
_psi_t_circuit = Qcircuit(VertExprArray(
_qpe_inputs, _qpe1_multigate,
[*multi_output_entries(_psi_t_ket, one, _t, (one, _t)),
*_u_outputs]))
_psi_t_circuit: 
In [59]:
_Psi_circuit = Qcircuit(VertExprArray(
_qpe_inputs, _qpe_multigate,
[*multi_output_entries(_Psi_ket, one, _t, (one, _t)), *_u_outputs]))
_Psi_circuit: 
In [60]:
_phase_circuit = Qcircuit(VertExprArray(
_qpe_inputs, _qpe_multigate,
[ExprRange(i, Measure(Z), one, _t), _s_wire],
[*multi_output_entries(NumKet(Mult(_two_pow_t, _phase), _t),
one, _t, (one, _t)),
*_u_outputs]))
_phase_circuit: 
In [61]:
_phase_est_circuit_b_r = Qcircuit(VertExprArray(
_qpe_inputs, _qpe_multigate,
[ExprRange(i, Measure(Z), one, _t), _s_wire],
[*multi_output_entries(NumKet(Mod(Round(Mult(_two_pow_t, _phase)), _two_pow_t), _t),
one, _t, (one, _t)),
*_u_outputs]))
_phase_est_circuit_b_r: 
In [62]:
_phase_est_circuit = Qcircuit(VertExprArray(
_qpe_inputs, _qpe_multigate,
[ExprRange(i, Measure(Z), one, _t), _s_wire],
[*multi_output_entries(NumKet(m, _t),
one, _t, (one, _t)),
*_u_outputs]))
_phase_est_circuit: 
In [63]:
t_wire = multi_wire(t)
s_wire = multi_wire(s)
s_wire:
In [64]:
QPE1_U_t_circuit = Qcircuit(VertExprArray(
ExprRange(i,
[ExprRange(j, ConditionalSet(
Conditional(
control_elem(Add(t, one)),
Equals(Add(Neg(i), t), j)),
Conditional(Gate(I), NotEquals(Add(Neg(i), t), j))),
one, t).with_case_simplification(),
*multi_gate_entries(MatrixExp(U, Exp(two, i)),
Add(t, one), Add(t, s), (one, s))],
subtract(t, one), zero, order='decreasing').with_case_simplification()))
QPE1_U_t_circuit: 
In [65]:
# This is incorrect (mod should be 2^t)
# _success_prob_e = Prob(LessEq(ModAbs(subtract(Mult(_two_pow_t, _phase_est), _b), one),
# e), _phase_est)
In [66]:
# the _ideal_phase_cond captures the case where the phase _phi can be
# represented exactly with the t bits (or fewer) available in the first register
_ideal_phase_cond = InSet(Mult(_two_pow_t, _phase),
Interval(zero, subtract(_two_pow_t, one)))
_ideal_phase_cond: 
In [67]:
_m_domain = Interval(zero, _two_pow_t__minus_one)
_m_domain: 
In [68]:
_success_cond = LessEq(ModAbs(subtract(frac(m, _two_pow_t), _phase), one),
Exp(two, Neg(_n)))
_success_cond: 
In [69]:
_Omega = Literal('Omega', r'\Omega')
_Omega: 
In [70]:
_sample_space = SetOfAll(m, _phase_est_circuit, domain=_m_domain)
_sample_space: 
In [71]:
_success_prob_e = ProbOfAll(m, _phase_est_circuit,
domain=_m_domain,
condition=LessEq(ModAbs(subtract(m, _b_floor), _two_pow_t), e)).with_wrapping()
_success_prob_e: 
In [72]:
# Corrected mod and switched back to m instead of phi
_fail_prob_e = ProbOfAll(m, _phase_est_circuit,
domain=_m_domain,
condition=greater(ModAbs(subtract(m, _b_floor), _two_pow_t), e)).with_wrapping()
_fail_prob_e: 
In [73]:
_Psi_register_meas = Qcircuit(VertExprArray(
[*multi_input_entries(_Psi_ket, one, _t, (one, _t))],
[ExprRange(k, Measure(Z), one, _t)],
[*multi_output_entries(NumKet(m, _t), one, _t, (one, _t))]))
_Psi_register_meas: 
In [74]:
# _success_prob_guarantee = greater_eq(_success_prob, subtract(one, _eps))
In [75]:
%end common