Expression of type Equals

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 ExprRange, 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, 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 = [s, t]
sub_expr3 = [U]
sub_expr4 = [var_ket_u]
sub_expr5 = [phase]
sub_expr6 = Add(t, one)
sub_expr7 = Add(t, s)
sub_expr8 = Interval(sub_expr6, sub_expr7)
sub_expr9 = Mult(two_pow_t, phase)
sub_expr10 = Unitary(two_pow_s)
sub_expr11 = MultiQubitElem(element = Gate(operation = QPE(U, t), part = sub_expr1), targets = Interval(one, sub_expr7))
sub_expr12 = InSet(sub_expr9, Interval(zero, subtract(two_pow_t, one)))
sub_expr13 = Equals(MatrixMult(U, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, phase)), var_ket_u))
sub_expr14 = 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_expr8), one, s)], [ExprRange(sub_expr1, sub_expr11, one, t), ExprRange(sub_expr1, sub_expr11, sub_expr6, sub_expr7)], [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_expr9, 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_expr8), one, s)]))), one)
expr = Equals(Forall(instance_param_or_params = sub_expr2, instance_expr = Forall(instance_param_or_params = sub_expr3, instance_expr = Forall(instance_param_or_params = sub_expr4, instance_expr = Forall(instance_param_or_params = sub_expr5, instance_expr = sub_expr14, domain = Real, conditions = [sub_expr12, sub_expr13, InSet(phase, IntervalCO(zero, one))]), domain = s_ket_domain, condition = normalized_var_ket_u), domain = sub_expr10), domain = NaturalPos), Forall(instance_param_or_params = sub_expr2, instance_expr = Forall(instance_param_or_params = sub_expr3, instance_expr = Forall(instance_param_or_params = sub_expr4, instance_expr = Forall(instance_param_or_params = sub_expr5, instance_expr = sub_expr14, domain = Real, conditions = [sub_expr12, sub_expr13]), domain = s_ket_domain, condition = normalized_var_ket_u), domain = sub_expr10), domain = 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[\forall_{s, t \in \mathbb{N}^+}~\left[\forall_{U \in \textrm{U}\left(2^{s}\right)}~\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]\right]\right]\right] = \left[\forall_{s, t \in \mathbb{N}^+}~\left[\forall_{U \in \textrm{U}\left(2^{s}\right)}~\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)}~\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]\right]\right]\right]

stored_expr.style_options()

name	description	default	current value	related methods
operation	'infix' or 'function' style formatting	infix	infix
wrap_positions	position(s) at which wrapping is to occur; '2 n - 1' is after the nth operand, '2 n' is after the nth operation.	()	()	('with_wrapping_at', 'with_wrap_before_operator', 'with_wrap_after_operator', 'without_wrapping', 'wrap_positions')
justification	if any wrap positions are set, justify to the 'left', 'center', or 'right'	center	center	('with_justification',)
direction	Direction of the relation (normal or reversed)	normal	normal	('with_direction_reversed', 'is_reversed')

# display the expression information
stored_expr.expr_info()

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