Expression of type Conditional

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, 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 = 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\{\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..

stored_expr.style_options()

name	description	default	current value	related methods
condition_delimiter	'comma' or 'and'	comma	comma	('with_comma_delimiter', 'with_conjunction_delimiter')

# display the expression information
stored_expr.expr_info()

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