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([U, var_ket_u, phase], 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(U, \lvert u \rangle, \varphi\right) \mapsto \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()

no style options

# display the expression information
stored_expr.expr_info()

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