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, s, t
from proveit.linear_algebra import MatrixMult, ScalarMult, Unitary
from proveit.logic import And, Equals, Forall, InSet
from proveit.numbers import Add, Exp, Interval, IntervalCO, Mod, Mult, NaturalPos, Real, Round, e, four, frac, greater, i, one, pi, 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 Prob

# 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, t], Conditional(Forall(instance_param_or_params = [U], instance_expr = Forall(instance_param_or_params = [var_ket_u], instance_expr = Forall(instance_param_or_params = [phase], instance_expr = greater(Prob(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(Mod(Round(Mult(two_pow_t, phase)), two_pow_t), 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)]))), frac(four, Exp(pi, two))), domain = Real, conditions = [InSet(phase, IntervalCO(zero, one)), Equals(MatrixMult(U, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, phase)), var_ket_u))]).with_wrapping(), domain = s_ket_domain, condition = normalized_var_ket_u).with_wrapping(), domain = Unitary(two_pow_s)).with_wrapping(), And(InSet(s, NaturalPos), InSet(t, NaturalPos))))

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(s, t\right) \mapsto \left\{\begin{array}{l}\forall_{U \in \textrm{U}\left(2^{s}\right)}~\\
\left[\begin{array}{l}\forall_{\lvert u \rangle \in \mathbb{C}^{2^{s}}~|~\left \|\lvert u \rangle\right \| = 1}~\\
\left[\begin{array}{l}\forall_{\varphi \in \mathbb{R}~|~\varphi \in \left[0,1\right), \left(U \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi} \cdot \lvert u \rangle\right)}~\\
\left(\textrm{Pr}\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \multigate{4}{\textrm{QPE}\left(U, t\right)} & \meter & \multiqout{3}{\lvert round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \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 round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right) > \frac{4}{\pi^{2}}\right)\end{array}\right]\end{array}\right]\end{array} \textrm{ if } s \in \mathbb{N}^+ ,  t \in \mathbb{N}^+\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	164, 178
2	Conditional	value: 3 condition: 4
3	Operation	operator: 26 operand: 7
4	Operation	operator: 42 operands: 6
5	ExprTuple	7
6	ExprTuple	8, 9
7	Lambda	parameter: 161 body: 11
8	Operation	operator: 60 operands: 12
9	Operation	operator: 60 operands: 13
10	ExprTuple	161
11	Conditional	value: 14 condition: 15
12	ExprTuple	164, 16
13	ExprTuple	178, 16
14	Operation	operator: 26 operand: 19
15	Operation	operator: 60 operands: 18
16	Literal
17	ExprTuple	19
18	ExprTuple	161, 20
19	Lambda	parameter: 150 body: 21
20	Operation	operator: 22 operand: 54
21	Conditional	value: 24 condition: 25
22	Literal
23	ExprTuple	54
24	Operation	operator: 26 operand: 29
25	Operation	operator: 42 operands: 28
26	Literal
27	ExprTuple	29
28	ExprTuple	30, 31
29	Lambda	parameter: 174 body: 33
30	Operation	operator: 60 operands: 34
31	Operation	operator: 62 operands: 35
32	ExprTuple	174
33	Conditional	value: 36 condition: 37
34	ExprTuple	150, 38
35	ExprTuple	39, 163
36	Operation	operator: 40 operands: 41
37	Operation	operator: 42 operands: 43
38	Operation	operator: 44 operands: 45
39	Operation	operator: 46 operand: 150
40	Literal
41	ExprTuple	48, 49
42	Literal
43	ExprTuple	50, 51, 52
44	Literal
45	ExprTuple	53, 54
46	Literal
47	ExprTuple	150
48	Operation	operator: 55 operands: 56
49	Operation	operator: 57 operand: 67
50	Operation	operator: 60 operands: 59
51	Operation	operator: 60 operands: 61
52	Operation	operator: 62 operands: 63
53	Literal
54	Operation	operator: 175 operands: 64
55	Literal
56	ExprTuple	65, 66
57	Literal
58	ExprTuple	67
59	ExprTuple	174, 68
60	Literal
61	ExprTuple	174, 69
62	Literal
63	ExprTuple	70, 71
64	ExprTuple	177, 164
65	Literal
66	Operation	operator: 175 operands: 72
67	Operation	operator: 73 operands: 74
68	Literal
69	Operation	operator: 75 operands: 76
70	Operation	operator: 77 operands: 78
71	Operation	operator: 79 operands: 80
72	ExprTuple	123, 177
73	Literal
74	ExprTuple	81, 82, 83, 84
75	Literal
76	ExprTuple	85, 163
77	Literal
78	ExprTuple	161, 150
79	Literal
80	ExprTuple	86, 150
81	ExprTuple	87, 88
82	ExprTuple	89, 90
83	ExprTuple	91, 92
84	ExprTuple	93, 94
85	Literal
86	Operation	operator: 175 operands: 95
87	ExprRange	lambda_map: 96 start_index: 163 end_index: 178
88	ExprRange	lambda_map: 97 start_index: 163 end_index: 164
89	ExprRange	lambda_map: 98 start_index: 163 end_index: 178
90	ExprRange	lambda_map: 98 start_index: 152 end_index: 153
91	ExprRange	lambda_map: 99 start_index: 163 end_index: 178
92	ExprRange	lambda_map: 100 start_index: 163 end_index: 164
93	ExprRange	lambda_map: 101 start_index: 163 end_index: 178
94	ExprRange	lambda_map: 102 start_index: 163 end_index: 164
95	ExprTuple	103, 104
96	Lambda	parameter: 151 body: 105
97	Lambda	parameter: 151 body: 106
98	Lambda	parameter: 151 body: 107
99	Lambda	parameter: 151 body: 108
100	Lambda	parameter: 151 body: 109
101	Lambda	parameter: 151 body: 110
102	Lambda	parameter: 151 body: 112
103	Literal
104	Operation	operator: 171 operands: 113
105	Operation	operator: 137 operands: 114
106	Operation	operator: 121 operands: 115
107	Operation	operator: 121 operands: 116
108	Operation	operator: 117 operands: 118
109	Operation	operator: 138 operands: 119
110	Operation	operator: 121 operands: 120
111	ExprTuple	151
112	Operation	operator: 121 operands: 122
113	ExprTuple	177, 123, 124, 174
114	NamedExprs	state: 125
115	NamedExprs	element: 126 targets: 134
116	NamedExprs	element: 127 targets: 128
117	Literal
118	NamedExprs	basis: 129
119	NamedExprs	operation: 130
120	NamedExprs	element: 131 targets: 132
121	Literal
122	NamedExprs	element: 133 targets: 134
123	Literal
124	Literal
125	Operation	operator: 135 operand: 147
126	Operation	operator: 137 operands: 144
127	Operation	operator: 138 operands: 139
128	Operation	operator: 145 operands: 140
129	Literal
130	Literal
131	Operation	operator: 143 operands: 141
132	Operation	operator: 145 operands: 142
133	Operation	operator: 143 operands: 144
134	Operation	operator: 145 operands: 146
135	Literal
136	ExprTuple	147
137	Literal
138	Literal
139	NamedExprs	operation: 148 part: 151
140	ExprTuple	163, 153
141	NamedExprs	state: 149 part: 151
142	ExprTuple	163, 178
143	Literal
144	NamedExprs	state: 150 part: 151
145	Literal
146	ExprTuple	152, 153
147	Literal
148	Operation	operator: 154 operands: 155
149	Operation	operator: 156 operands: 157
150	Variable
151	Variable
152	Operation	operator: 159 operands: 158
153	Operation	operator: 159 operands: 160
154	Literal
155	ExprTuple	161, 178
156	Literal
157	ExprTuple	162, 178
158	ExprTuple	178, 163
159	Literal
160	ExprTuple	178, 164
161	Variable
162	Operation	operator: 165 operands: 166
163	Literal
164	Variable
165	Literal
166	ExprTuple	167, 173
167	Operation	operator: 168 operand: 170
168	Literal
169	ExprTuple	170
170	Operation	operator: 171 operands: 172
171	Literal
172	ExprTuple	173, 174
173	Operation	operator: 175 operands: 176
174	Variable
175	Literal
176	ExprTuple	177, 178
177	Literal
178	Variable