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

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