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 Equals, Forall, InSet
from proveit.numbers import Add, Exp, Interval, IntervalCO, Mult, 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(U, Conditional(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)), InSet(phase, IntervalCO(zero, one))]), domain = s_ket_domain, condition = normalized_var_ket_u), InSet(U, Unitary(two_pow_s))))

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

U \mapsto \left\{\forall_{\lvert u \rangle \in \mathbb{C}^{2^{s}}~|~\left \|\lvert u \rangle\right \| = 1}~\left[\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), \varphi \in \left[0,1\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)\right] \textrm{ if } U \in \textrm{U}\left(2^{s}\right)\right..

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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