Expression of type Conditional ¶

from the theory of proveit.physics.quantum.QPE ¶

import proveit
# Automation is not needed when building an expression:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%load_expr # Load the stored expression as 'stored_expr'
# import Expression classes needed to build the expression
from proveit import Conditional, ExprRange, U, Variable, VertExprArray, s, t
from proveit.linear_algebra import MatrixMult, ScalarMult
from proveit.logic import And, Equals, InSet
from proveit.numbers import Add, Exp, Interval, Mult, Real, e, i, one, pi, subtract, two, zero
from proveit.physics.quantum import I, NumKet, Z, ket_plus, var_ket_u
from proveit.physics.quantum.QPE import QPE, phase, two_pow_t
from proveit.physics.quantum.circuits import Gate, Input, Measure, MultiQubitElem, Output, Qcircuit
from proveit.statistics import Prob

# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = Add(t, one)
sub_expr3 = Add(t, s)
sub_expr4 = Interval(sub_expr2, sub_expr3)
sub_expr5 = Mult(two_pow_t, phase)
sub_expr6 = MultiQubitElem(element = Gate(operation = QPE(U, t), part = sub_expr1), targets = Interval(one, sub_expr3))
expr = Conditional(Equals(Prob(Qcircuit(vert_expr_array = VertExprArray([ExprRange(sub_expr1, Input(state = ket_plus), one, t), ExprRange(sub_expr1, MultiQubitElem(element = Input(state = var_ket_u, part = sub_expr1), targets = sub_expr4), one, s)], [ExprRange(sub_expr1, sub_expr6, one, t), ExprRange(sub_expr1, sub_expr6, sub_expr2, sub_expr3)], [ExprRange(sub_expr1, Measure(basis = Z), one, t), ExprRange(sub_expr1, Gate(operation = I).with_implicit_representation(), one, s)], [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(sub_expr5, t), part = sub_expr1), targets = Interval(one, t)), one, t), ExprRange(sub_expr1, MultiQubitElem(element = Output(state = var_ket_u, part = sub_expr1), targets = sub_expr4), one, s)]))), one), And(InSet(phase, Real), InSet(sub_expr5, Interval(zero, subtract(two_pow_t, one))), Equals(MatrixMult(U, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, phase)), var_ket_u))))

# check that the built expression is the same as the stored expression
assert expr == stored_expr
assert expr._style_id == stored_expr._style_id
print("Passed sanity check: expr matches stored_expr")

Passed sanity check: expr matches stored_expr

# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())

\left\{\textrm{Pr}\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \multigate{4}{\textrm{QPE}\left(U, t\right)} & \meter & \multiqout{3}{\lvert 2^{t} \cdot \varphi \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert 2^{t} \cdot \varphi \rangle_{t}} \\
\qin{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} & \ghost{\textrm{QPE}\left(U, t\right)} & \measure{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} \qw & \ghostqout{\lvert 2^{t} \cdot \varphi \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert 2^{t} \cdot \varphi \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right) = 1 \textrm{ if } \varphi \in \mathbb{R} ,  \left(2^{t} \cdot \varphi\right) \in \{0~\ldotp \ldotp~2^{t} - 1\} ,  \left(U \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi} \cdot \lvert u \rangle\right)\right..

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions
0	Conditional	value: 1 condition: 2
1	Operation	operator: 15 operands: 3
2	Operation	operator: 4 operands: 5
3	ExprTuple	6, 116
4	Literal
5	ExprTuple	7, 8, 9
6	Operation	operator: 10 operand: 17
7	Operation	operator: 13 operands: 12
8	Operation	operator: 13 operands: 14
9	Operation	operator: 15 operands: 16
10	Literal
11	ExprTuple	17
12	ExprTuple	121, 18
13	Literal
14	ExprTuple	115, 19
15	Literal
16	ExprTuple	20, 21
17	Operation	operator: 22 operands: 23
18	Literal
19	Operation	operator: 98 operands: 24
20	Operation	operator: 25 operands: 26
21	Operation	operator: 27 operands: 28
22	Literal
23	ExprTuple	29, 30, 31, 32
24	ExprTuple	33, 34
25	Literal
26	ExprTuple	114, 103
27	Literal
28	ExprTuple	35, 103
29	ExprTuple	36, 37
30	ExprTuple	38, 39
31	ExprTuple	40, 41
32	ExprTuple	42, 43
33	Literal
34	Operation	operator: 112 operands: 44
35	Operation	operator: 122 operands: 45
36	ExprRange	lambda_map: 46 start_index: 116 end_index: 125
37	ExprRange	lambda_map: 47 start_index: 116 end_index: 117
38	ExprRange	lambda_map: 48 start_index: 116 end_index: 125
39	ExprRange	lambda_map: 48 start_index: 105 end_index: 106
40	ExprRange	lambda_map: 49 start_index: 116 end_index: 125
41	ExprRange	lambda_map: 50 start_index: 116 end_index: 117
42	ExprRange	lambda_map: 51 start_index: 116 end_index: 125
43	ExprRange	lambda_map: 52 start_index: 116 end_index: 117
44	ExprTuple	120, 53
45	ExprTuple	54, 55
46	Lambda	parameter: 104 body: 56
47	Lambda	parameter: 104 body: 57
48	Lambda	parameter: 104 body: 58
49	Lambda	parameter: 104 body: 59
50	Lambda	parameter: 104 body: 60
51	Lambda	parameter: 104 body: 61
52	Lambda	parameter: 104 body: 63
53	Operation	operator: 64 operand: 116
54	Literal
55	Operation	operator: 118 operands: 66
56	Operation	operator: 90 operands: 67
57	Operation	operator: 74 operands: 68
58	Operation	operator: 74 operands: 69
59	Operation	operator: 70 operands: 71
60	Operation	operator: 91 operands: 72
61	Operation	operator: 74 operands: 73
62	ExprTuple	104
63	Operation	operator: 74 operands: 75
64	Literal
65	ExprTuple	116
66	ExprTuple	124, 76, 77, 121
67	NamedExprs	state: 78
68	NamedExprs	element: 79 targets: 87
69	NamedExprs	element: 80 targets: 81
70	Literal
71	NamedExprs	basis: 82
72	NamedExprs	operation: 83
73	NamedExprs	element: 84 targets: 85
74	Literal
75	NamedExprs	element: 86 targets: 87
76	Literal
77	Literal
78	Operation	operator: 88 operand: 100
79	Operation	operator: 90 operands: 97
80	Operation	operator: 91 operands: 92
81	Operation	operator: 98 operands: 93
82	Literal
83	Literal
84	Operation	operator: 96 operands: 94
85	Operation	operator: 98 operands: 95
86	Operation	operator: 96 operands: 97
87	Operation	operator: 98 operands: 99
88	Literal
89	ExprTuple	100
90	Literal
91	Literal
92	NamedExprs	operation: 101 part: 104
93	ExprTuple	116, 106
94	NamedExprs	state: 102 part: 104
95	ExprTuple	116, 125
96	Literal
97	NamedExprs	state: 103 part: 104
98	Literal
99	ExprTuple	105, 106
100	Literal
101	Operation	operator: 107 operands: 108
102	Operation	operator: 109 operands: 110
103	Variable
104	Variable
105	Operation	operator: 112 operands: 111
106	Operation	operator: 112 operands: 113
107	Literal
108	ExprTuple	114, 125
109	Literal
110	ExprTuple	115, 125
111	ExprTuple	125, 116
112	Literal
113	ExprTuple	125, 117
114	Variable
115	Operation	operator: 118 operands: 119
116	Literal
117	Variable
118	Literal
119	ExprTuple	120, 121
120	Operation	operator: 122 operands: 123
121	Variable
122	Literal
123	ExprTuple	124, 125
124	Literal
125	Variable

Expression of type Conditional¶

from the theory of proveit.physics.quantum.QPE¶

Expression of type Conditional ¶

from the theory of proveit.physics.quantum.QPE ¶