logo

Expression of type And

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, U, Variable, VertExprArray, eps, m, n, s, t
from proveit.linear_algebra import MatrixMult, ScalarMult, Unitary
from proveit.logic import And, 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 = And(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()).with_wrapping_at(1,3)
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())

\begin{array}{c} \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}\right] \\  \land \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}~|~\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}\right] \\  \land \left[\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] \end{array}
In [5]:
stored_expr.style_options()
namedescriptiondefaultcurrent valuerelated methods
operation'infix' or 'function' style formattinginfixinfix
wrap_positionsposition(s) at which wrapping is to occur; '2 n - 1' is after the nth operand, '2 n' is after the nth operation.()(1 3)('with_wrapping_at', 'with_wrap_before_operator', 'with_wrap_after_operator', 'without_wrapping', 'wrap_positions')
justificationif any wrap positions are set, justify to the 'left', 'center', or 'right'centercenter('with_justification',)
In [6]:
# display the expression information
stored_expr.expr_info()
 core typesub-expressionsexpression
0Operationoperator: 166
operands: 1
1ExprTuple2, 3, 4
2Operationoperator: 64
operand: 8
3Operationoperator: 64
operand: 9
4Operationoperator: 64
operand: 10
5ExprTuple8
6ExprTuple9
7ExprTuple10
8Lambdaparameters: 12
body: 11
9Lambdaparameters: 12
body: 13
10Lambdaparameter: 302
body: 14
11Conditionalvalue: 15
condition: 17
12ExprTuple307, 318
13Conditionalvalue: 16
condition: 17
14Conditionalvalue: 18
condition: 19
15Operationoperator: 64
operand: 25
16Operationoperator: 64
operand: 26
17Operationoperator: 166
operands: 22
18Operationoperator: 64
operand: 27
19Operationoperator: 192
operands: 24
20ExprTuple25
21ExprTuple26
22ExprTuple46, 111
23ExprTuple27
24ExprTuple302, 28
25Lambdaparameter: 304
body: 29
26Lambdaparameter: 304
body: 31
27Lambdaparameters: 32
body: 33
28Operationoperator: 34
operands: 146
29Conditionalvalue: 35
condition: 70
30ExprTuple304
31Conditionalvalue: 36
condition: 70
32ExprTuple307, 277
33Conditionalvalue: 37
condition: 38
34Literal
35Operationoperator: 64
operand: 43
36Operationoperator: 64
operand: 44
37Operationoperator: 64
operand: 45
38Operationoperator: 166
operands: 42
39ExprTuple43
40ExprTuple44
41ExprTuple45
42ExprTuple46, 47, 48
43Lambdaparameter: 283
body: 49
44Lambdaparameter: 283
body: 50
45Lambdaparameters: 51
body: 52
46Operationoperator: 192
operands: 53
47Operationoperator: 192
operands: 54
48Operationoperator: 194
operands: 55
49Conditionalvalue: 56
condition: 58
50Conditionalvalue: 57
condition: 58
51ExprTuple304, 283, 314
52Conditionalvalue: 59
condition: 60
53ExprTuple307, 140
54ExprTuple277, 140
55ExprTuple317, 277
56Operationoperator: 64
operand: 67
57Operationoperator: 64
operand: 68
58Operationoperator: 166
operands: 63
59Operationoperator: 64
operand: 69
60Operationoperator: 166
operands: 66
61ExprTuple67
62ExprTuple68
63ExprTuple71, 72
64Literal
65ExprTuple69
66ExprTuple70, 71, 106, 107, 72, 108
67Lambdaparameter: 314
body: 73
68Lambdaparameter: 314
body: 74
69Lambdaparameter: 318
body: 76
70Operationoperator: 192
operands: 77
71Operationoperator: 192
operands: 78
72Operationoperator: 122
operands: 79
73Conditionalvalue: 80
condition: 81
74Conditionalvalue: 82
condition: 83
75ExprTuple318
76Conditionalvalue: 84
condition: 85
77ExprTuple304, 86
78ExprTuple283, 87
79ExprTuple88, 306
80Operationoperator: 122
operands: 89
81Operationoperator: 166
operands: 90
82Operationoperator: 91
operands: 92
83Operationoperator: 166
operands: 93
84Operationoperator: 194
operands: 94
85Operationoperator: 166
operands: 95
86Operationoperator: 96
operand: 114
87Operationoperator: 98
operands: 99
88Operationoperator: 100
operand: 283
89ExprTuple102, 306
90ExprTuple106, 103, 108
91Literal
92ExprTuple104, 105
93ExprTuple106, 107, 108
94ExprTuple109, 110
95ExprTuple111, 112
96Literal
97ExprTuple114
98Literal
99ExprTuple113, 114
100Literal
101ExprTuple283
102Operationoperator: 118
operand: 130
103Operationoperator: 192
operands: 116
104Operationoperator: 288
operands: 117
105Operationoperator: 118
operand: 133
106Operationoperator: 192
operands: 120
107Operationoperator: 192
operands: 121
108Operationoperator: 122
operands: 123
109Operationoperator: 300
operands: 124
110Operationoperator: 125
operand: 139
111Operationoperator: 192
operands: 127
112Operationoperator: 194
operands: 128
113Literal
114Operationoperator: 315
operands: 129
115ExprTuple130
116ExprTuple310, 209
117ExprTuple131, 132
118Literal
119ExprTuple133
120ExprTuple314, 134
121ExprTuple314, 135
122Literal
123ExprTuple136, 137
124ExprTuple306, 138
125Literal
126ExprTuple139
127ExprTuple318, 140
128ExprTuple141, 318
129ExprTuple317, 307
130Operationoperator: 164
operands: 142
131Literal
132Operationoperator: 315
operands: 143
133Operationoperator: 164
operands: 144
134Literal
135Operationoperator: 145
operands: 146
136Operationoperator: 147
operands: 148
137Operationoperator: 149
operands: 150
138Operationoperator: 290
operand: 302
139Lambdaparameter: 305
body: 153
140Literal
141Operationoperator: 300
operands: 154
142ExprTuple174, 175, 176, 155
143ExprTuple200, 317
144ExprTuple174, 175, 176, 156
145Literal
146ExprTuple239, 306
147Literal
148ExprTuple304, 283
149Literal
150ExprTuple157, 283
151ExprTuple302
152ExprTuple305
153Conditionalvalue: 158
condition: 159
154ExprTuple277, 160
155ExprTuple161, 191
156ExprTuple162, 191
157Operationoperator: 315
operands: 163
158Operationoperator: 164
operands: 165
159Operationoperator: 166
operands: 167
160Operationoperator: 168
operand: 180
161ExprRangelambda_map: 170
start_index: 306
end_index: 318
162ExprRangelambda_map: 171
start_index: 306
end_index: 318
163ExprTuple172, 173
164Literal
165ExprTuple174, 175, 176, 177
166Literal
167ExprTuple178, 179
168Literal
169ExprTuple180
170Lambdaparameter: 284
body: 181
171Lambdaparameter: 284
body: 182
172Literal
173Operationoperator: 311
operands: 183
174ExprTuple184, 185
175ExprTuple186, 187
176ExprTuple188, 189
177ExprTuple190, 191
178Operationoperator: 192
operands: 193
179Operationoperator: 194
operands: 195
180Operationoperator: 196
operands: 197
181Operationoperator: 237
operands: 198
182Operationoperator: 237
operands: 199
183ExprTuple317, 200, 201, 314
184ExprRangelambda_map: 202
start_index: 306
end_index: 318
185ExprRangelambda_map: 203
start_index: 306
end_index: 307
186ExprRangelambda_map: 204
start_index: 306
end_index: 318
187ExprRangelambda_map: 204
start_index: 285
end_index: 286
188ExprRangelambda_map: 205
start_index: 306
end_index: 318
189ExprRangelambda_map: 206
start_index: 306
end_index: 307
190ExprRangelambda_map: 207
start_index: 306
end_index: 318
191ExprRangelambda_map: 208
start_index: 306
end_index: 307
192Literal
193ExprTuple305, 209
194Literal
195ExprTuple210, 211
196Literal
197ExprTuple317, 212
198NamedExprselement: 213
targets: 253
199NamedExprselement: 214
targets: 253
200Literal
201Literal
202Lambdaparameter: 284
body: 215
203Lambdaparameter: 284
body: 216
204Lambdaparameter: 284
body: 217
205Lambdaparameter: 284
body: 218
206Lambdaparameter: 284
body: 219
207Lambdaparameter: 284
body: 220
208Lambdaparameter: 284
body: 222
209Operationoperator: 272
operands: 223
210Operationoperator: 224
operands: 225
211Operationoperator: 315
operands: 226
212Operationoperator: 300
operands: 227
213Operationoperator: 270
operands: 228
214Operationoperator: 270
operands: 229
215Operationoperator: 264
operands: 230
216Operationoperator: 237
operands: 231
217Operationoperator: 237
operands: 232
218Operationoperator: 233
operands: 234
219Operationoperator: 265
operands: 235
220Operationoperator: 237
operands: 236
221ExprTuple284
222Operationoperator: 237
operands: 238
223ExprTuple239, 240
224Literal
225ExprTuple241, 306
226ExprTuple317, 242
227ExprTuple317, 243
228NamedExprsstate: 244
part: 284
229NamedExprsstate: 245
part: 284
230NamedExprsstate: 246
231NamedExprselement: 247
targets: 255
232NamedExprselement: 248
targets: 249
233Literal
234NamedExprsbasis: 250
235NamedExprsoperation: 251
236NamedExprselement: 252
targets: 253
237Literal
238NamedExprselement: 254
targets: 255
239Literal
240Operationoperator: 300
operands: 256
241Operationoperator: 300
operands: 257
242Operationoperator: 290
operand: 277
243Operationoperator: 288
operands: 259
244Operationoperator: 297
operands: 260
245Operationoperator: 297
operands: 261
246Operationoperator: 262
operand: 280
247Operationoperator: 264
operands: 271
248Operationoperator: 265
operands: 266
249Operationoperator: 272
operands: 267
250Literal
251Literal
252Operationoperator: 270
operands: 268
253Operationoperator: 272
operands: 269
254Operationoperator: 270
operands: 271
255Operationoperator: 272
operands: 273
256ExprTuple313, 274
257ExprTuple275, 276
258ExprTuple277
259ExprTuple306, 278
260ExprTuple310, 318
261ExprTuple279, 318
262Literal
263ExprTuple280
264Literal
265Literal
266NamedExprsoperation: 281
part: 284
267ExprTuple306, 286
268NamedExprsstate: 282
part: 284
269ExprTuple306, 318
270Literal
271NamedExprsstate: 283
part: 284
272Literal
273ExprTuple285, 286
274Operationoperator: 290
operand: 306
275Operationoperator: 288
operands: 289
276Operationoperator: 290
operand: 314
277Variable
278Operationoperator: 311
operands: 292
279Operationoperator: 293
operands: 294
280Literal
281Operationoperator: 295
operands: 296
282Operationoperator: 297
operands: 298
283Variable
284Variable
285Operationoperator: 300
operands: 299
286Operationoperator: 300
operands: 301
287ExprTuple306
288Literal
289ExprTuple305, 313
290Literal
291ExprTuple314
292ExprTuple317, 302
293Literal
294ExprTuple303, 313
295Literal
296ExprTuple304, 318
297Literal
298ExprTuple305, 318
299ExprTuple318, 306
300Literal
301ExprTuple318, 307
302Variable
303Operationoperator: 308
operand: 310
304Variable
305Variable
306Literal
307Variable
308Literal
309ExprTuple310
310Operationoperator: 311
operands: 312
311Literal
312ExprTuple313, 314
313Operationoperator: 315
operands: 316
314Variable
315Literal
316ExprTuple317, 318
317Literal
318Variable