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 And, 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 = ExprTuple(Lambda([s, n], Conditional(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(), And(InSet(s, NaturalPos), InSet(n, NaturalPos), greater_eq(n, two)))))

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