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 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 = Lambda([s, n], 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))))

# 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(s, n\right) \mapsto \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()

# display the expression information
stored_expr.expr_info()

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