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([U, var_ket_u, phase], Conditional(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(), And(InSet(U, Unitary(two_pow_s)), InSet(var_ket_u, s_ket_domain), InSet(phase, Real), 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))))))

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