Theorem main_theorems_combined of type And ¶

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

import proveit
# Automation is not needed when only building an expression:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%load_theorem_expr # Load the stored theorem expression as 'stored_expr'
# import the special expression
from proveit.physics.quantum.QPE import main_theorems_combined

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

Passed sanity check: main_theorems_combined matches stored_expr

# 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}

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

name	description	default	current value	related methods
operation	'infix' or 'function' style formatting	infix	infix
wrap_positions	position(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')
justification	if any wrap positions are set, justify to the 'left', 'center', or 'right'	center	center	('with_justification',)

	core type	sub-expressions
0	Operation	operator: 166 operands: 1
1	ExprTuple	2, 3, 4
2	Operation	operator: 64 operand: 8
3	Operation	operator: 64 operand: 9
4	Operation	operator: 64 operand: 10
5	ExprTuple	8
6	ExprTuple	9
7	ExprTuple	10
8	Lambda	parameters: 12 body: 11
9	Lambda	parameters: 12 body: 13
10	Lambda	parameter: 302 body: 14
11	Conditional	value: 15 condition: 17
12	ExprTuple	307, 318
13	Conditional	value: 16 condition: 17
14	Conditional	value: 18 condition: 19
15	Operation	operator: 64 operand: 25
16	Operation	operator: 64 operand: 26
17	Operation	operator: 166 operands: 22
18	Operation	operator: 64 operand: 27
19	Operation	operator: 192 operands: 24
20	ExprTuple	25
21	ExprTuple	26
22	ExprTuple	46, 111
23	ExprTuple	27
24	ExprTuple	302, 28
25	Lambda	parameter: 304 body: 29
26	Lambda	parameter: 304 body: 31
27	Lambda	parameters: 32 body: 33
28	Operation	operator: 34 operands: 146
29	Conditional	value: 35 condition: 70
30	ExprTuple	304
31	Conditional	value: 36 condition: 70
32	ExprTuple	307, 277
33	Conditional	value: 37 condition: 38
34	Literal
35	Operation	operator: 64 operand: 43
36	Operation	operator: 64 operand: 44
37	Operation	operator: 64 operand: 45
38	Operation	operator: 166 operands: 42
39	ExprTuple	43
40	ExprTuple	44
41	ExprTuple	45
42	ExprTuple	46, 47, 48
43	Lambda	parameter: 283 body: 49
44	Lambda	parameter: 283 body: 50
45	Lambda	parameters: 51 body: 52
46	Operation	operator: 192 operands: 53
47	Operation	operator: 192 operands: 54
48	Operation	operator: 194 operands: 55
49	Conditional	value: 56 condition: 58
50	Conditional	value: 57 condition: 58
51	ExprTuple	304, 283, 314
52	Conditional	value: 59 condition: 60
53	ExprTuple	307, 140
54	ExprTuple	277, 140
55	ExprTuple	317, 277
56	Operation	operator: 64 operand: 67
57	Operation	operator: 64 operand: 68
58	Operation	operator: 166 operands: 63
59	Operation	operator: 64 operand: 69
60	Operation	operator: 166 operands: 66
61	ExprTuple	67
62	ExprTuple	68
63	ExprTuple	71, 72
64	Literal
65	ExprTuple	69
66	ExprTuple	70, 71, 106, 107, 72, 108
67	Lambda	parameter: 314 body: 73
68	Lambda	parameter: 314 body: 74
69	Lambda	parameter: 318 body: 76
70	Operation	operator: 192 operands: 77
71	Operation	operator: 192 operands: 78
72	Operation	operator: 122 operands: 79
73	Conditional	value: 80 condition: 81
74	Conditional	value: 82 condition: 83
75	ExprTuple	318
76	Conditional	value: 84 condition: 85
77	ExprTuple	304, 86
78	ExprTuple	283, 87
79	ExprTuple	88, 306
80	Operation	operator: 122 operands: 89
81	Operation	operator: 166 operands: 90
82	Operation	operator: 91 operands: 92
83	Operation	operator: 166 operands: 93
84	Operation	operator: 194 operands: 94
85	Operation	operator: 166 operands: 95
86	Operation	operator: 96 operand: 114
87	Operation	operator: 98 operands: 99
88	Operation	operator: 100 operand: 283
89	ExprTuple	102, 306
90	ExprTuple	106, 103, 108
91	Literal
92	ExprTuple	104, 105
93	ExprTuple	106, 107, 108
94	ExprTuple	109, 110
95	ExprTuple	111, 112
96	Literal
97	ExprTuple	114
98	Literal
99	ExprTuple	113, 114
100	Literal
101	ExprTuple	283
102	Operation	operator: 118 operand: 130
103	Operation	operator: 192 operands: 116
104	Operation	operator: 288 operands: 117
105	Operation	operator: 118 operand: 133
106	Operation	operator: 192 operands: 120
107	Operation	operator: 192 operands: 121
108	Operation	operator: 122 operands: 123
109	Operation	operator: 300 operands: 124
110	Operation	operator: 125 operand: 139
111	Operation	operator: 192 operands: 127
112	Operation	operator: 194 operands: 128
113	Literal
114	Operation	operator: 315 operands: 129
115	ExprTuple	130
116	ExprTuple	310, 209
117	ExprTuple	131, 132
118	Literal
119	ExprTuple	133
120	ExprTuple	314, 134
121	ExprTuple	314, 135
122	Literal
123	ExprTuple	136, 137
124	ExprTuple	306, 138
125	Literal
126	ExprTuple	139
127	ExprTuple	318, 140
128	ExprTuple	141, 318
129	ExprTuple	317, 307
130	Operation	operator: 164 operands: 142
131	Literal
132	Operation	operator: 315 operands: 143
133	Operation	operator: 164 operands: 144
134	Literal
135	Operation	operator: 145 operands: 146
136	Operation	operator: 147 operands: 148
137	Operation	operator: 149 operands: 150
138	Operation	operator: 290 operand: 302
139	Lambda	parameter: 305 body: 153
140	Literal
141	Operation	operator: 300 operands: 154
142	ExprTuple	174, 175, 176, 155
143	ExprTuple	200, 317
144	ExprTuple	174, 175, 176, 156
145	Literal
146	ExprTuple	239, 306
147	Literal
148	ExprTuple	304, 283
149	Literal
150	ExprTuple	157, 283
151	ExprTuple	302
152	ExprTuple	305
153	Conditional	value: 158 condition: 159
154	ExprTuple	277, 160
155	ExprTuple	161, 191
156	ExprTuple	162, 191
157	Operation	operator: 315 operands: 163
158	Operation	operator: 164 operands: 165
159	Operation	operator: 166 operands: 167
160	Operation	operator: 168 operand: 180
161	ExprRange	lambda_map: 170 start_index: 306 end_index: 318
162	ExprRange	lambda_map: 171 start_index: 306 end_index: 318
163	ExprTuple	172, 173
164	Literal
165	ExprTuple	174, 175, 176, 177
166	Literal
167	ExprTuple	178, 179
168	Literal
169	ExprTuple	180
170	Lambda	parameter: 284 body: 181
171	Lambda	parameter: 284 body: 182
172	Literal
173	Operation	operator: 311 operands: 183
174	ExprTuple	184, 185
175	ExprTuple	186, 187
176	ExprTuple	188, 189
177	ExprTuple	190, 191
178	Operation	operator: 192 operands: 193
179	Operation	operator: 194 operands: 195
180	Operation	operator: 196 operands: 197
181	Operation	operator: 237 operands: 198
182	Operation	operator: 237 operands: 199
183	ExprTuple	317, 200, 201, 314
184	ExprRange	lambda_map: 202 start_index: 306 end_index: 318
185	ExprRange	lambda_map: 203 start_index: 306 end_index: 307
186	ExprRange	lambda_map: 204 start_index: 306 end_index: 318
187	ExprRange	lambda_map: 204 start_index: 285 end_index: 286
188	ExprRange	lambda_map: 205 start_index: 306 end_index: 318
189	ExprRange	lambda_map: 206 start_index: 306 end_index: 307
190	ExprRange	lambda_map: 207 start_index: 306 end_index: 318
191	ExprRange	lambda_map: 208 start_index: 306 end_index: 307
192	Literal
193	ExprTuple	305, 209
194	Literal
195	ExprTuple	210, 211
196	Literal
197	ExprTuple	317, 212
198	NamedExprs	element: 213 targets: 253
199	NamedExprs	element: 214 targets: 253
200	Literal
201	Literal
202	Lambda	parameter: 284 body: 215
203	Lambda	parameter: 284 body: 216
204	Lambda	parameter: 284 body: 217
205	Lambda	parameter: 284 body: 218
206	Lambda	parameter: 284 body: 219
207	Lambda	parameter: 284 body: 220
208	Lambda	parameter: 284 body: 222
209	Operation	operator: 272 operands: 223
210	Operation	operator: 224 operands: 225
211	Operation	operator: 315 operands: 226
212	Operation	operator: 300 operands: 227
213	Operation	operator: 270 operands: 228
214	Operation	operator: 270 operands: 229
215	Operation	operator: 264 operands: 230
216	Operation	operator: 237 operands: 231
217	Operation	operator: 237 operands: 232
218	Operation	operator: 233 operands: 234
219	Operation	operator: 265 operands: 235
220	Operation	operator: 237 operands: 236
221	ExprTuple	284
222	Operation	operator: 237 operands: 238
223	ExprTuple	239, 240
224	Literal
225	ExprTuple	241, 306
226	ExprTuple	317, 242
227	ExprTuple	317, 243
228	NamedExprs	state: 244 part: 284
229	NamedExprs	state: 245 part: 284
230	NamedExprs	state: 246
231	NamedExprs	element: 247 targets: 255
232	NamedExprs	element: 248 targets: 249
233	Literal
234	NamedExprs	basis: 250
235	NamedExprs	operation: 251
236	NamedExprs	element: 252 targets: 253
237	Literal
238	NamedExprs	element: 254 targets: 255
239	Literal
240	Operation	operator: 300 operands: 256
241	Operation	operator: 300 operands: 257
242	Operation	operator: 290 operand: 277
243	Operation	operator: 288 operands: 259
244	Operation	operator: 297 operands: 260
245	Operation	operator: 297 operands: 261
246	Operation	operator: 262 operand: 280
247	Operation	operator: 264 operands: 271
248	Operation	operator: 265 operands: 266
249	Operation	operator: 272 operands: 267
250	Literal
251	Literal
252	Operation	operator: 270 operands: 268
253	Operation	operator: 272 operands: 269
254	Operation	operator: 270 operands: 271
255	Operation	operator: 272 operands: 273
256	ExprTuple	313, 274
257	ExprTuple	275, 276
258	ExprTuple	277
259	ExprTuple	306, 278
260	ExprTuple	310, 318
261	ExprTuple	279, 318
262	Literal
263	ExprTuple	280
264	Literal
265	Literal
266	NamedExprs	operation: 281 part: 284
267	ExprTuple	306, 286
268	NamedExprs	state: 282 part: 284
269	ExprTuple	306, 318
270	Literal
271	NamedExprs	state: 283 part: 284
272	Literal
273	ExprTuple	285, 286
274	Operation	operator: 290 operand: 306
275	Operation	operator: 288 operands: 289
276	Operation	operator: 290 operand: 314
277	Variable
278	Operation	operator: 311 operands: 292
279	Operation	operator: 293 operands: 294
280	Literal
281	Operation	operator: 295 operands: 296
282	Operation	operator: 297 operands: 298
283	Variable
284	Variable
285	Operation	operator: 300 operands: 299
286	Operation	operator: 300 operands: 301
287	ExprTuple	306
288	Literal
289	ExprTuple	305, 313
290	Literal
291	ExprTuple	314
292	ExprTuple	317, 302
293	Literal
294	ExprTuple	303, 313
295	Literal
296	ExprTuple	304, 318
297	Literal
298	ExprTuple	305, 318
299	ExprTuple	318, 306
300	Literal
301	ExprTuple	318, 307
302	Variable
303	Operation	operator: 308 operand: 310
304	Variable
305	Variable
306	Literal
307	Variable
308	Literal
309	ExprTuple	310
310	Operation	operator: 311 operands: 312
311	Literal
312	ExprTuple	313, 314
313	Operation	operator: 315 operands: 316
314	Variable
315	Literal
316	ExprTuple	317, 318
317	Literal
318	Variable

Theorem main_theorems_combined of type And¶

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

Theorem main_theorems_combined of type And ¶

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