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