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, 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 = [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()

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_{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}

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