Expression of type Lambda ¶

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, Lambda, 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 = Lambda(eps, 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))))

# 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())

\epsilon \mapsto \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()

# display the expression information
stored_expr.expr_info()

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

Expression of type Lambda¶

from the theory of proveit.physics.quantum.QPE¶

Expression of type Lambda ¶

from the theory of proveit.physics.quantum.QPE ¶