Expression of type Forall

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 ExprRange, 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, ModAbs, Mult, NaturalPos, Neg, Real, e, frac, 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 ProbOfAll

# 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 = 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([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(m, 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)])), domain = Interval(zero, subtract(two_pow_t, one)), 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 = [Unitary(two_pow_s), s_ket_domain, Real], conditions = [InSet(phase, IntervalCO(zero, one)), normalized_var_ket_u, Equals(MatrixMult(U, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, phase)), var_ket_u))]).with_wrapping(), domain = NaturalPos, condition = greater_eq(n, two)).with_wrapping(), domain = IntervalOC(zero, one)).with_wrapping()

expr:

# 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())

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

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	parameter: 219 body: 3
3	Conditional	value: 4 condition: 5
4	Operation	operator: 28 operand: 8
5	Operation	operator: 121 operands: 7
6	ExprTuple	8
7	ExprTuple	219, 9
8	Lambda	parameters: 10 body: 11
9	Operation	operator: 12 operands: 63
10	ExprTuple	223, 194
11	Conditional	value: 13 condition: 14
12	Literal
13	Operation	operator: 28 operand: 17
14	Operation	operator: 102 operands: 16
15	ExprTuple	17
16	ExprTuple	18, 19, 20
17	Lambda	parameters: 21 body: 22
18	Operation	operator: 121 operands: 23
19	Operation	operator: 121 operands: 24
20	Operation	operator: 123 operands: 25
21	ExprTuple	220, 199, 218
22	Conditional	value: 26 condition: 27
23	ExprTuple	223, 86
24	ExprTuple	194, 86
25	ExprTuple	226, 194
26	Operation	operator: 28 operand: 31
27	Operation	operator: 102 operands: 30
28	Literal
29	ExprTuple	31
30	ExprTuple	32, 33, 34, 35, 36, 37
31	Lambda	parameter: 227 body: 39
32	Operation	operator: 121 operands: 40
33	Operation	operator: 121 operands: 41
34	Operation	operator: 121 operands: 42
35	Operation	operator: 121 operands: 43
36	Operation	operator: 45 operands: 44
37	Operation	operator: 45 operands: 46
38	ExprTuple	227
39	Conditional	value: 47 condition: 48
40	ExprTuple	220, 49
41	ExprTuple	199, 50
42	ExprTuple	218, 51
43	ExprTuple	218, 52
44	ExprTuple	53, 222
45	Literal
46	ExprTuple	54, 55
47	Operation	operator: 123 operands: 56
48	Operation	operator: 102 operands: 57
49	Operation	operator: 58 operand: 75
50	Operation	operator: 60 operands: 61
51	Literal
52	Operation	operator: 62 operands: 63
53	Operation	operator: 64 operand: 199
54	Operation	operator: 66 operands: 67
55	Operation	operator: 68 operands: 69
56	ExprTuple	70, 71
57	ExprTuple	72, 73
58	Literal
59	ExprTuple	75
60	Literal
61	ExprTuple	74, 75
62	Literal
63	ExprTuple	160, 222
64	Literal
65	ExprTuple	199
66	Literal
67	ExprTuple	220, 199
68	Literal
69	ExprTuple	76, 199
70	Operation	operator: 215 operands: 77
71	Operation	operator: 78 operand: 85
72	Operation	operator: 121 operands: 80
73	Operation	operator: 123 operands: 81
74	Literal
75	Operation	operator: 224 operands: 82
76	Operation	operator: 224 operands: 83
77	ExprTuple	222, 84
78	Literal
79	ExprTuple	85
80	ExprTuple	227, 86
81	ExprTuple	87, 227
82	ExprTuple	226, 223
83	ExprTuple	88, 89
84	Operation	operator: 206 operand: 219
85	Lambda	parameter: 221 body: 92
86	Literal
87	Operation	operator: 215 operands: 93
88	Literal
89	Operation	operator: 208 operands: 94
90	ExprTuple	219
91	ExprTuple	221
92	Conditional	value: 95 condition: 96
93	ExprTuple	194, 97
94	ExprTuple	226, 98, 99, 218
95	Operation	operator: 100 operands: 101
96	Operation	operator: 102 operands: 103
97	Operation	operator: 104 operand: 112
98	Literal
99	Literal
100	Literal
101	ExprTuple	106, 107, 108, 109
102	Literal
103	ExprTuple	110, 111
104	Literal
105	ExprTuple	112
106	ExprTuple	113, 114
107	ExprTuple	115, 116
108	ExprTuple	117, 118
109	ExprTuple	119, 120
110	Operation	operator: 121 operands: 122
111	Operation	operator: 123 operands: 124
112	Operation	operator: 125 operands: 126
113	ExprRange	lambda_map: 127 start_index: 222 end_index: 227
114	ExprRange	lambda_map: 128 start_index: 222 end_index: 223
115	ExprRange	lambda_map: 129 start_index: 222 end_index: 227
116	ExprRange	lambda_map: 129 start_index: 201 end_index: 202
117	ExprRange	lambda_map: 130 start_index: 222 end_index: 227
118	ExprRange	lambda_map: 131 start_index: 222 end_index: 223
119	ExprRange	lambda_map: 132 start_index: 222 end_index: 227
120	ExprRange	lambda_map: 133 start_index: 222 end_index: 223
121	Literal
122	ExprTuple	221, 134
123	Literal
124	ExprTuple	135, 136
125	Literal
126	ExprTuple	226, 137
127	Lambda	parameter: 200 body: 138
128	Lambda	parameter: 200 body: 139
129	Lambda	parameter: 200 body: 140
130	Lambda	parameter: 200 body: 141
131	Lambda	parameter: 200 body: 142
132	Lambda	parameter: 200 body: 143
133	Lambda	parameter: 200 body: 145
134	Operation	operator: 189 operands: 146
135	Operation	operator: 147 operands: 148
136	Operation	operator: 224 operands: 149
137	Operation	operator: 215 operands: 150
138	Operation	operator: 181 operands: 151
139	Operation	operator: 158 operands: 152
140	Operation	operator: 158 operands: 153
141	Operation	operator: 154 operands: 155
142	Operation	operator: 182 operands: 156
143	Operation	operator: 158 operands: 157
144	ExprTuple	200
145	Operation	operator: 158 operands: 159
146	ExprTuple	160, 161
147	Literal
148	ExprTuple	162, 222
149	ExprTuple	226, 163
150	ExprTuple	226, 164
151	NamedExprs	state: 165
152	NamedExprs	element: 166 targets: 174
153	NamedExprs	element: 167 targets: 168
154	Literal
155	NamedExprs	basis: 169
156	NamedExprs	operation: 170
157	NamedExprs	element: 171 targets: 172
158	Literal
159	NamedExprs	element: 173 targets: 174
160	Literal
161	Operation	operator: 215 operands: 175
162	Operation	operator: 215 operands: 176
163	Operation	operator: 206 operand: 194
164	Operation	operator: 204 operands: 178
165	Operation	operator: 179 operand: 196
166	Operation	operator: 181 operands: 188
167	Operation	operator: 182 operands: 183
168	Operation	operator: 189 operands: 184
169	Literal
170	Literal
171	Operation	operator: 187 operands: 185
172	Operation	operator: 189 operands: 186
173	Operation	operator: 187 operands: 188
174	Operation	operator: 189 operands: 190
175	ExprTuple	217, 191
176	ExprTuple	192, 193
177	ExprTuple	194
178	ExprTuple	222, 195
179	Literal
180	ExprTuple	196
181	Literal
182	Literal
183	NamedExprs	operation: 197 part: 200
184	ExprTuple	222, 202
185	NamedExprs	state: 198 part: 200
186	ExprTuple	222, 227
187	Literal
188	NamedExprs	state: 199 part: 200
189	Literal
190	ExprTuple	201, 202
191	Operation	operator: 206 operand: 222
192	Operation	operator: 204 operands: 205
193	Operation	operator: 206 operand: 218
194	Variable
195	Operation	operator: 208 operands: 209
196	Literal
197	Operation	operator: 210 operands: 211
198	Operation	operator: 212 operands: 213
199	Variable
200	Variable
201	Operation	operator: 215 operands: 214
202	Operation	operator: 215 operands: 216
203	ExprTuple	222
204	Literal
205	ExprTuple	221, 217
206	Literal
207	ExprTuple	218
208	Literal
209	ExprTuple	226, 219
210	Literal
211	ExprTuple	220, 227
212	Literal
213	ExprTuple	221, 227
214	ExprTuple	227, 222
215	Literal
216	ExprTuple	227, 223
217	Operation	operator: 224 operands: 225
218	Variable
219	Variable
220	Variable
221	Variable
222	Literal
223	Variable
224	Literal
225	ExprTuple	226, 227
226	Literal
227	Variable