Expression of type ExprTuple

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 Conditional, ExprRange, ExprTuple, Lambda, 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 = ExprTuple(Lambda(eps, Conditional(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(), InSet(eps, IntervalOC(zero, one)))))

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

\left(\epsilon \mapsto \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} \textrm{ if } \epsilon \in \left(0,1\right]\right..\right)

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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