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, Unitary
from proveit.logic import Equals, Forall, InSet
from proveit.numbers import Add, Exp, Interval, IntervalCO, Mod, Mult, Real, Round, e, four, frac, greater, i, one, pi, two, zero
from proveit.physics.quantum import I, NumKet, Z, ket_plus, normalized_var_ket_u, var_ket_u
from proveit.physics.quantum.QPE import QPE, phase, s_ket_domain, two_pow_s, 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 = MultiQubitElem(element = Gate(operation = QPE(U, t), part = sub_expr1), targets = Interval(one, sub_expr3))
expr = Conditional(Forall(instance_param_or_params = [var_ket_u], instance_expr = Forall(instance_param_or_params = [phase], instance_expr = greater(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_expr5, one, t), ExprRange(sub_expr1, sub_expr5, 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(Mod(Round(Mult(two_pow_t, phase)), two_pow_t), 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)]))), frac(four, Exp(pi, two))), domain = Real, conditions = [InSet(phase, IntervalCO(zero, one)), Equals(MatrixMult(U, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, phase)), var_ket_u))]).with_wrapping(), domain = s_ket_domain, condition = normalized_var_ket_u).with_wrapping(), InSet(U, Unitary(two_pow_s)))

# 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\{\begin{array}{l}\forall_{\lvert u \rangle \in \mathbb{C}^{2^{s}}~|~\left \|\lvert u \rangle\right \| = 1}~\\
\left[\begin{array}{l}\forall_{\varphi \in \mathbb{R}~|~\varphi \in \left[0,1\right), \left(U \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi} \cdot \lvert u \rangle\right)}~\\
\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 round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \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 round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right) > \frac{4}{\pi^{2}}\right)\end{array}\right]\end{array} \textrm{ if } U \in \textrm{U}\left(2^{s}\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: 12 operand: 5
2	Operation	operator: 46 operands: 4
3	ExprTuple	5
4	ExprTuple	147, 6
5	Lambda	parameter: 136 body: 7
6	Operation	operator: 8 operand: 40
7	Conditional	value: 10 condition: 11
8	Literal
9	ExprTuple	40
10	Operation	operator: 12 operand: 15
11	Operation	operator: 28 operands: 14
12	Literal
13	ExprTuple	15
14	ExprTuple	16, 17
15	Lambda	parameter: 160 body: 19
16	Operation	operator: 46 operands: 20
17	Operation	operator: 48 operands: 21
18	ExprTuple	160
19	Conditional	value: 22 condition: 23
20	ExprTuple	136, 24
21	ExprTuple	25, 149
22	Operation	operator: 26 operands: 27
23	Operation	operator: 28 operands: 29
24	Operation	operator: 30 operands: 31
25	Operation	operator: 32 operand: 136
26	Literal
27	ExprTuple	34, 35
28	Literal
29	ExprTuple	36, 37, 38
30	Literal
31	ExprTuple	39, 40
32	Literal
33	ExprTuple	136
34	Operation	operator: 41 operands: 42
35	Operation	operator: 43 operand: 53
36	Operation	operator: 46 operands: 45
37	Operation	operator: 46 operands: 47
38	Operation	operator: 48 operands: 49
39	Literal
40	Operation	operator: 161 operands: 50
41	Literal
42	ExprTuple	51, 52
43	Literal
44	ExprTuple	53
45	ExprTuple	160, 54
46	Literal
47	ExprTuple	160, 55
48	Literal
49	ExprTuple	56, 57
50	ExprTuple	163, 150
51	Literal
52	Operation	operator: 161 operands: 58
53	Operation	operator: 59 operands: 60
54	Literal
55	Operation	operator: 61 operands: 62
56	Operation	operator: 63 operands: 64
57	Operation	operator: 65 operands: 66
58	ExprTuple	109, 163
59	Literal
60	ExprTuple	67, 68, 69, 70
61	Literal
62	ExprTuple	71, 149
63	Literal
64	ExprTuple	147, 136
65	Literal
66	ExprTuple	72, 136
67	ExprTuple	73, 74
68	ExprTuple	75, 76
69	ExprTuple	77, 78
70	ExprTuple	79, 80
71	Literal
72	Operation	operator: 161 operands: 81
73	ExprRange	lambda_map: 82 start_index: 149 end_index: 164
74	ExprRange	lambda_map: 83 start_index: 149 end_index: 150
75	ExprRange	lambda_map: 84 start_index: 149 end_index: 164
76	ExprRange	lambda_map: 84 start_index: 138 end_index: 139
77	ExprRange	lambda_map: 85 start_index: 149 end_index: 164
78	ExprRange	lambda_map: 86 start_index: 149 end_index: 150
79	ExprRange	lambda_map: 87 start_index: 149 end_index: 164
80	ExprRange	lambda_map: 88 start_index: 149 end_index: 150
81	ExprTuple	89, 90
82	Lambda	parameter: 137 body: 91
83	Lambda	parameter: 137 body: 92
84	Lambda	parameter: 137 body: 93
85	Lambda	parameter: 137 body: 94
86	Lambda	parameter: 137 body: 95
87	Lambda	parameter: 137 body: 96
88	Lambda	parameter: 137 body: 98
89	Literal
90	Operation	operator: 157 operands: 99
91	Operation	operator: 123 operands: 100
92	Operation	operator: 107 operands: 101
93	Operation	operator: 107 operands: 102
94	Operation	operator: 103 operands: 104
95	Operation	operator: 124 operands: 105
96	Operation	operator: 107 operands: 106
97	ExprTuple	137
98	Operation	operator: 107 operands: 108
99	ExprTuple	163, 109, 110, 160
100	NamedExprs	state: 111
101	NamedExprs	element: 112 targets: 120
102	NamedExprs	element: 113 targets: 114
103	Literal
104	NamedExprs	basis: 115
105	NamedExprs	operation: 116
106	NamedExprs	element: 117 targets: 118
107	Literal
108	NamedExprs	element: 119 targets: 120
109	Literal
110	Literal
111	Operation	operator: 121 operand: 133
112	Operation	operator: 123 operands: 130
113	Operation	operator: 124 operands: 125
114	Operation	operator: 131 operands: 126
115	Literal
116	Literal
117	Operation	operator: 129 operands: 127
118	Operation	operator: 131 operands: 128
119	Operation	operator: 129 operands: 130
120	Operation	operator: 131 operands: 132
121	Literal
122	ExprTuple	133
123	Literal
124	Literal
125	NamedExprs	operation: 134 part: 137
126	ExprTuple	149, 139
127	NamedExprs	state: 135 part: 137
128	ExprTuple	149, 164
129	Literal
130	NamedExprs	state: 136 part: 137
131	Literal
132	ExprTuple	138, 139
133	Literal
134	Operation	operator: 140 operands: 141
135	Operation	operator: 142 operands: 143
136	Variable
137	Variable
138	Operation	operator: 145 operands: 144
139	Operation	operator: 145 operands: 146
140	Literal
141	ExprTuple	147, 164
142	Literal
143	ExprTuple	148, 164
144	ExprTuple	164, 149
145	Literal
146	ExprTuple	164, 150
147	Variable
148	Operation	operator: 151 operands: 152
149	Literal
150	Variable
151	Literal
152	ExprTuple	153, 159
153	Operation	operator: 154 operand: 156
154	Literal
155	ExprTuple	156
156	Operation	operator: 157 operands: 158
157	Literal
158	ExprTuple	159, 160
159	Operation	operator: 161 operands: 162
160	Variable
161	Literal
162	ExprTuple	163, 164
163	Literal
164	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 ¶