Expression of type Forall

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, eps, m, n, s, t
from proveit.linear_algebra import MatrixMult, ScalarMult, Unitary
from proveit.logic import 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 = Forall(instance_param_or_params = [U, var_ket_u, phase], instance_expr = 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(), domains = [Unitary(two_pow_s), s_ket_domain, Real], conditions = [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))]).with_wrapping()

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

\begin{array}{l}\forall_{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)}~\\
\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}\right]\end{array}

stored_expr.style_options()

name	description	default	current value	related methods
with_wrapping	If 'True', wrap the Expression after the parameters	None	True	('with_wrapping',)
condition_wrapping	Wrap 'before' or 'after' the condition (or None).	None	None/False	('with_wrap_after_condition', 'with_wrap_before_condition')
wrap_params	If 'True', wraps every two parameters AND wraps the Expression after the parameters	None	None/False	('with_params',)
justification	justify to the 'left', 'center', or 'right' in the array cells	center	center	('with_justification',)

# display the expression information
stored_expr.expr_info()

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