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

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