logo

Expression of type ExprTuple

from the theory of proveit.physics.quantum.QPE

In [1]:
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 ExprRange, ExprTuple, U, Variable, VertExprArray, eps, m, n, s, t
from proveit.linear_algebra import MatrixMult, ScalarMult, Unitary
from proveit.logic import Equals, Forall, InSet
from proveit.numbers import Add, Ceil, Exp, Interval, IntervalCO, IntervalOC, LessEq, Log, Mod, ModAbs, Mult, NaturalPos, Neg, Real, Round, e, four, frac, greater, greater_eq, i, one, pi, subtract, 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, ProbOfAll
In [2]:
# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = [s, t]
sub_expr3 = [U]
sub_expr4 = [var_ket_u]
sub_expr5 = [phase]
sub_expr6 = Add(t, one)
sub_expr7 = Add(t, s)
sub_expr8 = Interval(one, t)
sub_expr9 = Interval(sub_expr6, sub_expr7)
sub_expr10 = Mult(two_pow_t, phase)
sub_expr11 = Unitary(two_pow_s)
sub_expr12 = InSet(phase, IntervalCO(zero, one))
sub_expr13 = [ExprRange(sub_expr1, Measure(basis = Z), one, t), ExprRange(sub_expr1, Gate(operation = I).with_implicit_representation(), one, s)]
sub_expr14 = MultiQubitElem(element = Gate(operation = QPE(U, t), part = sub_expr1), targets = Interval(one, sub_expr7))
sub_expr15 = Interval(zero, subtract(two_pow_t, one))
sub_expr16 = ExprRange(sub_expr1, MultiQubitElem(element = Output(state = var_ket_u, part = sub_expr1), targets = sub_expr9), one, s)
sub_expr17 = Equals(MatrixMult(U, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, phase)), var_ket_u))
sub_expr18 = [ExprRange(sub_expr1, Input(state = ket_plus), one, t), ExprRange(sub_expr1, MultiQubitElem(element = Input(state = var_ket_u, part = sub_expr1), targets = sub_expr9), one, s)]
sub_expr19 = [ExprRange(sub_expr1, sub_expr14, one, t), ExprRange(sub_expr1, sub_expr14, sub_expr6, sub_expr7)]
expr = ExprTuple(Forall(instance_param_or_params = sub_expr2, instance_expr = Forall(instance_param_or_params = sub_expr3, instance_expr = Forall(instance_param_or_params = sub_expr4, instance_expr = Forall(instance_param_or_params = sub_expr5, instance_expr = Equals(Prob(Qcircuit(vert_expr_array = VertExprArray(sub_expr18, sub_expr19, sub_expr13, [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(sub_expr10, t), part = sub_expr1), targets = sub_expr8), one, t), sub_expr16]))), one), domain = Real, conditions = [InSet(sub_expr10, sub_expr15), sub_expr17]).with_wrapping(), domain = s_ket_domain, condition = normalized_var_ket_u).with_wrapping(), domain = sub_expr11).with_wrapping(), domain = NaturalPos).with_wrapping(), Forall(instance_param_or_params = sub_expr2, instance_expr = Forall(instance_param_or_params = sub_expr3, instance_expr = Forall(instance_param_or_params = sub_expr4, instance_expr = Forall(instance_param_or_params = sub_expr5, instance_expr = greater(Prob(Qcircuit(vert_expr_array = VertExprArray(sub_expr18, sub_expr19, sub_expr13, [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(Mod(Round(sub_expr10), two_pow_t), t), part = sub_expr1), targets = sub_expr8), one, t), sub_expr16]))), frac(four, Exp(pi, two))), domain = Real, conditions = [sub_expr12, sub_expr17]).with_wrapping(), domain = s_ket_domain, condition = normalized_var_ket_u).with_wrapping(), domain = sub_expr11).with_wrapping(), domain = NaturalPos).with_wrapping(), Forall(instance_param_or_params = [eps], instance_expr = Forall(instance_param_or_params = [s, n], instance_expr = Forall(instance_param_or_params = [U, var_ket_u, phase], instance_expr = Forall(instance_param_or_params = [t], instance_expr = greater_eq(ProbOfAll(instance_param_or_params = [m], instance_element = Qcircuit(vert_expr_array = VertExprArray(sub_expr18, sub_expr19, sub_expr13, [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(m, t), part = sub_expr1), targets = sub_expr8), one, t), sub_expr16])), domain = sub_expr15, condition = LessEq(ModAbs(subtract(frac(m, two_pow_t), phase), one), Exp(two, Neg(n)))).with_wrapping(), subtract(one, eps)), domain = NaturalPos, condition = greater_eq(t, Add(n, Ceil(Log(two, Add(two, frac(one, Mult(two, eps)))))))).with_wrapping(), domains = [sub_expr11, s_ket_domain, Real], conditions = [sub_expr12, normalized_var_ket_u, sub_expr17]).with_wrapping(), domain = NaturalPos, condition = greater_eq(n, two)).with_wrapping(), domain = IntervalOC(zero, one)).with_wrapping())
expr:
In [3]:
# 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
In [4]:
# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())

\left(\begin{array}{l}\forall_{s, t \in \mathbb{N}^+}~\\
\left[\begin{array}{l}\forall_{U \in \textrm{U}\left(2^{s}\right)}~\\
\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}~|~\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)}~\\
\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\right)\end{array}\right]\end{array}\right]\end{array}\right]\end{array}, \begin{array}{l}\forall_{s, t \in \mathbb{N}^+}~\\
\left[\begin{array}{l}\forall_{U \in \textrm{U}\left(2^{s}\right)}~\\
\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}\right]\end{array}\right]\end{array}, \begin{array}{l}\forall_{\epsilon \in \left(0,1\right]}~\\
\left[\begin{array}{l}\forall_{s, n \in \mathbb{N}^+~|~n \geq 2}~\\
\left[\begin{array}{l}\forall_{U \in \textrm{U}\left(2^{s}\right), \lvert u \rangle \in \mathbb{C}^{2^{s}}, \varphi \in \mathbb{R}~|~\varphi \in \left[0,1\right), \left \|\lvert u \rangle\right \| = 1, \left(U \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi} \cdot \lvert u \rangle\right)}~\\
\left[\begin{array}{l}\forall_{t \in \mathbb{N}^+~|~t \geq \left(n + \left\lceil \textrm{log}_2\left(2 + \frac{1}{2 \cdot \epsilon}\right)\right\rceil\right)}~\\
\left(\left[\begin{array}{l}\textrm{Prob}_{m \in \{0~\ldotp \ldotp~2^{t} - 1\}~|~\left|\frac{m}{2^{t}} - \varphi\right|_{\textup{mod}\thinspace 1} \leq 2^{-n}}~\\
\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \multigate{4}{\textrm{QPE}\left(U, t\right)} & \meter & \multiqout{3}{\lvert m \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert m \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 m \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert m \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right)\end{array}\right] \geq \left(1 - \epsilon\right)\right)\end{array}\right]\end{array}\right]\end{array}\right]\end{array}\right)
In [5]:
stored_expr.style_options()
namedescriptiondefaultcurrent valuerelated methods
wrap_positionsposition(s) at which wrapping is to occur; 'n' is after the nth comma.()()('with_wrapping_at',)
justificationif any wrap positions are set, justify to the 'left', 'center', or 'right'leftleft('with_justification',)
In [6]:
# display the expression information
stored_expr.expr_info()
 core typesub-expressionsexpression
0ExprTuple1, 2, 3
1Operationoperator: 63
operand: 7
2Operationoperator: 63
operand: 8
3Operationoperator: 63
operand: 9
4ExprTuple7
5ExprTuple8
6ExprTuple9
7Lambdaparameters: 11
body: 10
8Lambdaparameters: 11
body: 12
9Lambdaparameter: 301
body: 13
10Conditionalvalue: 14
condition: 16
11ExprTuple306, 317
12Conditionalvalue: 15
condition: 16
13Conditionalvalue: 17
condition: 18
14Operationoperator: 63
operand: 24
15Operationoperator: 63
operand: 25
16Operationoperator: 165
operands: 21
17Operationoperator: 63
operand: 26
18Operationoperator: 191
operands: 23
19ExprTuple24
20ExprTuple25
21ExprTuple45, 110
22ExprTuple26
23ExprTuple301, 27
24Lambdaparameter: 303
body: 28
25Lambdaparameter: 303
body: 30
26Lambdaparameters: 31
body: 32
27Operationoperator: 33
operands: 145
28Conditionalvalue: 34
condition: 69
29ExprTuple303
30Conditionalvalue: 35
condition: 69
31ExprTuple306, 276
32Conditionalvalue: 36
condition: 37
33Literal
34Operationoperator: 63
operand: 42
35Operationoperator: 63
operand: 43
36Operationoperator: 63
operand: 44
37Operationoperator: 165
operands: 41
38ExprTuple42
39ExprTuple43
40ExprTuple44
41ExprTuple45, 46, 47
42Lambdaparameter: 282
body: 48
43Lambdaparameter: 282
body: 49
44Lambdaparameters: 50
body: 51
45Operationoperator: 191
operands: 52
46Operationoperator: 191
operands: 53
47Operationoperator: 193
operands: 54
48Conditionalvalue: 55
condition: 57
49Conditionalvalue: 56
condition: 57
50ExprTuple303, 282, 313
51Conditionalvalue: 58
condition: 59
52ExprTuple306, 139
53ExprTuple276, 139
54ExprTuple316, 276
55Operationoperator: 63
operand: 66
56Operationoperator: 63
operand: 67
57Operationoperator: 165
operands: 62
58Operationoperator: 63
operand: 68
59Operationoperator: 165
operands: 65
60ExprTuple66
61ExprTuple67
62ExprTuple70, 71
63Literal
64ExprTuple68
65ExprTuple69, 70, 105, 106, 71, 107
66Lambdaparameter: 313
body: 72
67Lambdaparameter: 313
body: 73
68Lambdaparameter: 317
body: 75
69Operationoperator: 191
operands: 76
70Operationoperator: 191
operands: 77
71Operationoperator: 121
operands: 78
72Conditionalvalue: 79
condition: 80
73Conditionalvalue: 81
condition: 82
74ExprTuple317
75Conditionalvalue: 83
condition: 84
76ExprTuple303, 85
77ExprTuple282, 86
78ExprTuple87, 305
79Operationoperator: 121
operands: 88
80Operationoperator: 165
operands: 89
81Operationoperator: 90
operands: 91
82Operationoperator: 165
operands: 92
83Operationoperator: 193
operands: 93
84Operationoperator: 165
operands: 94
85Operationoperator: 95
operand: 113
86Operationoperator: 97
operands: 98
87Operationoperator: 99
operand: 282
88ExprTuple101, 305
89ExprTuple105, 102, 107
90Literal
91ExprTuple103, 104
92ExprTuple105, 106, 107
93ExprTuple108, 109
94ExprTuple110, 111
95Literal
96ExprTuple113
97Literal
98ExprTuple112, 113
99Literal
100ExprTuple282
101Operationoperator: 117
operand: 129
102Operationoperator: 191
operands: 115
103Operationoperator: 287
operands: 116
104Operationoperator: 117
operand: 132
105Operationoperator: 191
operands: 119
106Operationoperator: 191
operands: 120
107Operationoperator: 121
operands: 122
108Operationoperator: 299
operands: 123
109Operationoperator: 124
operand: 138
110Operationoperator: 191
operands: 126
111Operationoperator: 193
operands: 127
112Literal
113Operationoperator: 314
operands: 128
114ExprTuple129
115ExprTuple309, 208
116ExprTuple130, 131
117Literal
118ExprTuple132
119ExprTuple313, 133
120ExprTuple313, 134
121Literal
122ExprTuple135, 136
123ExprTuple305, 137
124Literal
125ExprTuple138
126ExprTuple317, 139
127ExprTuple140, 317
128ExprTuple316, 306
129Operationoperator: 163
operands: 141
130Literal
131Operationoperator: 314
operands: 142
132Operationoperator: 163
operands: 143
133Literal
134Operationoperator: 144
operands: 145
135Operationoperator: 146
operands: 147
136Operationoperator: 148
operands: 149
137Operationoperator: 289
operand: 301
138Lambdaparameter: 304
body: 152
139Literal
140Operationoperator: 299
operands: 153
141ExprTuple173, 174, 175, 154
142ExprTuple199, 316
143ExprTuple173, 174, 175, 155
144Literal
145ExprTuple238, 305
146Literal
147ExprTuple303, 282
148Literal
149ExprTuple156, 282
150ExprTuple301
151ExprTuple304
152Conditionalvalue: 157
condition: 158
153ExprTuple276, 159
154ExprTuple160, 190
155ExprTuple161, 190
156Operationoperator: 314
operands: 162
157Operationoperator: 163
operands: 164
158Operationoperator: 165
operands: 166
159Operationoperator: 167
operand: 179
160ExprRangelambda_map: 169
start_index: 305
end_index: 317
161ExprRangelambda_map: 170
start_index: 305
end_index: 317
162ExprTuple171, 172
163Literal
164ExprTuple173, 174, 175, 176
165Literal
166ExprTuple177, 178
167Literal
168ExprTuple179
169Lambdaparameter: 283
body: 180
170Lambdaparameter: 283
body: 181
171Literal
172Operationoperator: 310
operands: 182
173ExprTuple183, 184
174ExprTuple185, 186
175ExprTuple187, 188
176ExprTuple189, 190
177Operationoperator: 191
operands: 192
178Operationoperator: 193
operands: 194
179Operationoperator: 195
operands: 196
180Operationoperator: 236
operands: 197
181Operationoperator: 236
operands: 198
182ExprTuple316, 199, 200, 313
183ExprRangelambda_map: 201
start_index: 305
end_index: 317
184ExprRangelambda_map: 202
start_index: 305
end_index: 306
185ExprRangelambda_map: 203
start_index: 305
end_index: 317
186ExprRangelambda_map: 203
start_index: 284
end_index: 285
187ExprRangelambda_map: 204
start_index: 305
end_index: 317
188ExprRangelambda_map: 205
start_index: 305
end_index: 306
189ExprRangelambda_map: 206
start_index: 305
end_index: 317
190ExprRangelambda_map: 207
start_index: 305
end_index: 306
191Literal
192ExprTuple304, 208
193Literal
194ExprTuple209, 210
195Literal
196ExprTuple316, 211
197NamedExprselement: 212
targets: 252
198NamedExprselement: 213
targets: 252
199Literal
200Literal
201Lambdaparameter: 283
body: 214
202Lambdaparameter: 283
body: 215
203Lambdaparameter: 283
body: 216
204Lambdaparameter: 283
body: 217
205Lambdaparameter: 283
body: 218
206Lambdaparameter: 283
body: 219
207Lambdaparameter: 283
body: 221
208Operationoperator: 271
operands: 222
209Operationoperator: 223
operands: 224
210Operationoperator: 314
operands: 225
211Operationoperator: 299
operands: 226
212Operationoperator: 269
operands: 227
213Operationoperator: 269
operands: 228
214Operationoperator: 263
operands: 229
215Operationoperator: 236
operands: 230
216Operationoperator: 236
operands: 231
217Operationoperator: 232
operands: 233
218Operationoperator: 264
operands: 234
219Operationoperator: 236
operands: 235
220ExprTuple283
221Operationoperator: 236
operands: 237
222ExprTuple238, 239
223Literal
224ExprTuple240, 305
225ExprTuple316, 241
226ExprTuple316, 242
227NamedExprsstate: 243
part: 283
228NamedExprsstate: 244
part: 283
229NamedExprsstate: 245
230NamedExprselement: 246
targets: 254
231NamedExprselement: 247
targets: 248
232Literal
233NamedExprsbasis: 249
234NamedExprsoperation: 250
235NamedExprselement: 251
targets: 252
236Literal
237NamedExprselement: 253
targets: 254
238Literal
239Operationoperator: 299
operands: 255
240Operationoperator: 299
operands: 256
241Operationoperator: 289
operand: 276
242Operationoperator: 287
operands: 258
243Operationoperator: 296
operands: 259
244Operationoperator: 296
operands: 260
245Operationoperator: 261
operand: 279
246Operationoperator: 263
operands: 270
247Operationoperator: 264
operands: 265
248Operationoperator: 271
operands: 266
249Literal
250Literal
251Operationoperator: 269
operands: 267
252Operationoperator: 271
operands: 268
253Operationoperator: 269
operands: 270
254Operationoperator: 271
operands: 272
255ExprTuple312, 273
256ExprTuple274, 275
257ExprTuple276
258ExprTuple305, 277
259ExprTuple309, 317
260ExprTuple278, 317
261Literal
262ExprTuple279
263Literal
264Literal
265NamedExprsoperation: 280
part: 283
266ExprTuple305, 285
267NamedExprsstate: 281
part: 283
268ExprTuple305, 317
269Literal
270NamedExprsstate: 282
part: 283
271Literal
272ExprTuple284, 285
273Operationoperator: 289
operand: 305
274Operationoperator: 287
operands: 288
275Operationoperator: 289
operand: 313
276Variable
277Operationoperator: 310
operands: 291
278Operationoperator: 292
operands: 293
279Literal
280Operationoperator: 294
operands: 295
281Operationoperator: 296
operands: 297
282Variable
283Variable
284Operationoperator: 299
operands: 298
285Operationoperator: 299
operands: 300
286ExprTuple305
287Literal
288ExprTuple304, 312
289Literal
290ExprTuple313
291ExprTuple316, 301
292Literal
293ExprTuple302, 312
294Literal
295ExprTuple303, 317
296Literal
297ExprTuple304, 317
298ExprTuple317, 305
299Literal
300ExprTuple317, 306
301Variable
302Operationoperator: 307
operand: 309
303Variable
304Variable
305Literal
306Variable
307Literal
308ExprTuple309
309Operationoperator: 310
operands: 311
310Literal
311ExprTuple312, 313
312Operationoperator: 314
operands: 315
313Variable
314Literal
315ExprTuple316, 317
316Literal
317Variable