Theorem qpe_best_guarantee of type Forall

from the theory of proveit.physics.quantum.QPE

see dependencies

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 qpe_best_guarantee

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

Passed sanity check: qpe_best_guarantee matches stored_expr

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

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

stored_expr.style_options()

name	description	default	current value	related methods
with_wrapping	If 'True', wrap the Expression after the parameters	None	True	('with_wrapping',)
condition_wrapping	Wrap 'before' or 'after' the condition (or None).	None	None/False	('with_wrap_after_condition', 'with_wrap_before_condition')
wrap_params	If 'True', wraps every two parameters AND wraps the Expression after the parameters	None	None/False	('with_params',)
justification	justify to the 'left', 'center', or 'right' in the array cells	center	center	('with_justification',)

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions	expression
0	Operation	operator: 28 operand: 2
1	ExprTuple	2
2	Lambda	parameters: 3 body: 4
3	ExprTuple	166, 180
4	Conditional	value: 5 condition: 6
5	Operation	operator: 28 operand: 9
6	Operation	operator: 44 operands: 8
7	ExprTuple	9
8	ExprTuple	10, 11
9	Lambda	parameter: 163 body: 13
10	Operation	operator: 62 operands: 14
11	Operation	operator: 62 operands: 15
12	ExprTuple	163
13	Conditional	value: 16 condition: 17
14	ExprTuple	166, 18
15	ExprTuple	180, 18
16	Operation	operator: 28 operand: 21
17	Operation	operator: 62 operands: 20
18	Literal
19	ExprTuple	21
20	ExprTuple	163, 22
21	Lambda	parameter: 152 body: 23
22	Operation	operator: 24 operand: 56
23	Conditional	value: 26 condition: 27
24	Literal
25	ExprTuple	56
26	Operation	operator: 28 operand: 31
27	Operation	operator: 44 operands: 30
28	Literal
29	ExprTuple	31
30	ExprTuple	32, 33
31	Lambda	parameter: 176 body: 35
32	Operation	operator: 62 operands: 36
33	Operation	operator: 64 operands: 37
34	ExprTuple	176
35	Conditional	value: 38 condition: 39
36	ExprTuple	152, 40
37	ExprTuple	41, 165
38	Operation	operator: 42 operands: 43
39	Operation	operator: 44 operands: 45
40	Operation	operator: 46 operands: 47
41	Operation	operator: 48 operand: 152
42	Literal
43	ExprTuple	50, 51
44	Literal
45	ExprTuple	52, 53, 54
46	Literal
47	ExprTuple	55, 56
48	Literal
49	ExprTuple	152
50	Operation	operator: 57 operands: 58
51	Operation	operator: 59 operand: 69
52	Operation	operator: 62 operands: 61
53	Operation	operator: 62 operands: 63
54	Operation	operator: 64 operands: 65
55	Literal
56	Operation	operator: 177 operands: 66
57	Literal
58	ExprTuple	67, 68
59	Literal
60	ExprTuple	69
61	ExprTuple	176, 70
62	Literal
63	ExprTuple	176, 71
64	Literal
65	ExprTuple	72, 73
66	ExprTuple	179, 166
67	Literal
68	Operation	operator: 177 operands: 74
69	Operation	operator: 75 operands: 76
70	Literal
71	Operation	operator: 77 operands: 78
72	Operation	operator: 79 operands: 80
73	Operation	operator: 81 operands: 82
74	ExprTuple	125, 179
75	Literal
76	ExprTuple	83, 84, 85, 86
77	Literal
78	ExprTuple	87, 165
79	Literal
80	ExprTuple	163, 152
81	Literal
82	ExprTuple	88, 152
83	ExprTuple	89, 90
84	ExprTuple	91, 92
85	ExprTuple	93, 94
86	ExprTuple	95, 96
87	Literal
88	Operation	operator: 177 operands: 97
89	ExprRange	lambda_map: 98 start_index: 165 end_index: 180
90	ExprRange	lambda_map: 99 start_index: 165 end_index: 166
91	ExprRange	lambda_map: 100 start_index: 165 end_index: 180
92	ExprRange	lambda_map: 100 start_index: 154 end_index: 155
93	ExprRange	lambda_map: 101 start_index: 165 end_index: 180
94	ExprRange	lambda_map: 102 start_index: 165 end_index: 166
95	ExprRange	lambda_map: 103 start_index: 165 end_index: 180
96	ExprRange	lambda_map: 104 start_index: 165 end_index: 166
97	ExprTuple	105, 106
98	Lambda	parameter: 153 body: 107
99	Lambda	parameter: 153 body: 108
100	Lambda	parameter: 153 body: 109
101	Lambda	parameter: 153 body: 110
102	Lambda	parameter: 153 body: 111
103	Lambda	parameter: 153 body: 112
104	Lambda	parameter: 153 body: 114
105	Literal
106	Operation	operator: 173 operands: 115
107	Operation	operator: 139 operands: 116
108	Operation	operator: 123 operands: 117
109	Operation	operator: 123 operands: 118
110	Operation	operator: 119 operands: 120
111	Operation	operator: 140 operands: 121
112	Operation	operator: 123 operands: 122
113	ExprTuple	153
114	Operation	operator: 123 operands: 124
115	ExprTuple	179, 125, 126, 176
116	NamedExprs	state: 127
117	NamedExprs	element: 128 targets: 136
118	NamedExprs	element: 129 targets: 130
119	Literal
120	NamedExprs	basis: 131
121	NamedExprs	operation: 132
122	NamedExprs	element: 133 targets: 134
123	Literal
124	NamedExprs	element: 135 targets: 136
125	Literal
126	Literal
127	Operation	operator: 137 operand: 149
128	Operation	operator: 139 operands: 146
129	Operation	operator: 140 operands: 141
130	Operation	operator: 147 operands: 142
131	Literal
132	Literal
133	Operation	operator: 145 operands: 143
134	Operation	operator: 147 operands: 144
135	Operation	operator: 145 operands: 146
136	Operation	operator: 147 operands: 148
137	Literal
138	ExprTuple	149
139	Literal
140	Literal
141	NamedExprs	operation: 150 part: 153
142	ExprTuple	165, 155
143	NamedExprs	state: 151 part: 153
144	ExprTuple	165, 180
145	Literal
146	NamedExprs	state: 152 part: 153
147	Literal
148	ExprTuple	154, 155
149	Literal
150	Operation	operator: 156 operands: 157
151	Operation	operator: 158 operands: 159
152	Variable
153	Variable
154	Operation	operator: 161 operands: 160
155	Operation	operator: 161 operands: 162
156	Literal
157	ExprTuple	163, 180
158	Literal
159	ExprTuple	164, 180
160	ExprTuple	180, 165
161	Literal
162	ExprTuple	180, 166
163	Variable
164	Operation	operator: 167 operands: 168
165	Literal
166	Variable
167	Literal
168	ExprTuple	169, 175
169	Operation	operator: 170 operand: 172
170	Literal
171	ExprTuple	172
172	Operation	operator: 173 operands: 174
173	Literal
174	ExprTuple	175, 176
175	Operation	operator: 177 operands: 178
176	Variable
177	Literal
178	ExprTuple	179, 180
179	Literal
180	Variable