Expression of type Forall

from the theory of proveit.physics.quantum.circuits

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, IndexedVar, U, Variable, m, t
from proveit.linear_algebra import MatrixMult, ScalarMult, Unitary
from proveit.logic import Equals, Forall
from proveit.numbers import Exp, Mult, NaturalPos, e, i, one, pi, two
from proveit.physics.quantum import m_ket_domain, normalized_var_ket_u, var_ket_u, varphi
from proveit.physics.quantum.circuits import phase_kickback_on_register_circuit
from proveit.statistics import Prob

# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = IndexedVar(U, sub_expr1)
sub_expr3 = IndexedVar(varphi, sub_expr1)
expr = Forall(instance_param_or_params = [m, t], instance_expr = Forall(instance_param_or_params = [ExprRange(sub_expr1, sub_expr2, one, t)], instance_expr = Forall(instance_param_or_params = [var_ket_u], instance_expr = Forall(instance_param_or_params = [ExprRange(sub_expr1, sub_expr3, one, t)], instance_expr = Equals(Prob(phase_kickback_on_register_circuit), one), condition = ExprRange(sub_expr1, Equals(MatrixMult(sub_expr2, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, sub_expr3)), var_ket_u)), one, t)).with_wrapping(), domain = m_ket_domain, condition = normalized_var_ket_u).with_wrapping(), domain = Unitary(Exp(two, m))).with_wrapping(), domain = NaturalPos).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_{m, t \in \mathbb{N}^+}~\\
\left[\begin{array}{l}\forall_{U_{1}, U_{2}, \ldots, U_{t} \in \textrm{U}\left(2^{m}\right)}~\\
\left[\begin{array}{l}\forall_{\lvert u \rangle \in \mathbb{C}^{2^{m}}~|~\left \|\lvert u \rangle\right \| = 1}~\\
\left[\begin{array}{l}\forall_{\varphi_{1}, \varphi_{2}, \ldots, \varphi_{t}~|~\left(\left(U_{1} \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{1}} \cdot \lvert u \rangle\right)\right), \left(\left(U_{2} \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{2}} \cdot \lvert u \rangle\right)\right), \ldots, \left(\left(U_{t} \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{t}} \cdot \lvert u \rangle\right)\right)}~\\
\left(\textrm{Pr}\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \control{} \qw \qwx[1] & \qw & \gate{\cdots} \qwx[1] & \qw & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{1}} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\lvert + \rangle} & \qw \qwx[1] & \control{} \qw \qwx[1] & \gate{\cdots} \qwx[1] & \qw & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{2}} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} & \gate{\vdots} \qwx[1] & \gate{\vdots} \qwx[1] & \gate{\ddots} \qwx[1] & \gate{\vdots} & \qout{\vdots} \\
\qin{\lvert + \rangle} & \qw \qwx[1] & \qw \qwx[1] & \gate{\cdots} \qwx[1] & \control{} \qw \qwx[1] & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{t}} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\lvert u \rangle} & \gate{U_{1}} & \gate{U_{2}} & \gate{\cdots} & \gate{U_{t}} & \qout{\lvert u \rangle}
} \end{array}\right) = 1\right)\end{array}\right]\end{array}\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: 30 operand: 2
1	ExprTuple	2
2	Lambda	parameters: 3 body: 4
3	ExprTuple	159, 175
4	Conditional	value: 5 condition: 6
5	Operation	operator: 30 operand: 9
6	Operation	operator: 52 operands: 8
7	ExprTuple	9
8	ExprTuple	10, 11
9	Lambda	parameters: 12 body: 13
10	Operation	operator: 40 operands: 14
11	Operation	operator: 40 operands: 15
12	ExprTuple	16
13	Conditional	value: 17 condition: 18
14	ExprTuple	159, 19
15	ExprTuple	175, 19
16	ExprRange	lambda_map: 20 start_index: 176 end_index: 175
17	Operation	operator: 30 operand: 23
18	Operation	operator: 52 operands: 22
19	Literal
20	Lambda	parameter: 185 body: 89
21	ExprTuple	23
22	ExprTuple	24
23	Lambda	parameter: 123 body: 25
24	ExprRange	lambda_map: 26 start_index: 176 end_index: 175
25	Conditional	value: 27 condition: 28
26	Lambda	parameter: 185 body: 29
27	Operation	operator: 30 operand: 34
28	Operation	operator: 52 operands: 32
29	Operation	operator: 40 operands: 33
30	Literal
31	ExprTuple	34
32	ExprTuple	35, 36
33	ExprTuple	89, 37
34	Lambda	parameters: 38 body: 39
35	Operation	operator: 40 operands: 41
36	Operation	operator: 136 operands: 42
37	Operation	operator: 43 operand: 61
38	ExprTuple	45
39	Conditional	value: 46 condition: 47
40	Literal
41	ExprTuple	123, 48
42	ExprTuple	49, 176
43	Literal
44	ExprTuple	61
45	ExprRange	lambda_map: 50 start_index: 176 end_index: 175
46	Operation	operator: 136 operands: 51
47	Operation	operator: 52 operands: 53
48	Operation	operator: 54 operands: 55
49	Operation	operator: 56 operand: 123
50	Lambda	parameter: 185 body: 182
51	ExprTuple	58, 176
52	Literal
53	ExprTuple	59
54	Literal
55	ExprTuple	60, 61
56	Literal
57	ExprTuple	123
58	Operation	operator: 62 operand: 66
59	ExprRange	lambda_map: 64 start_index: 176 end_index: 175
60	Literal
61	Operation	operator: 167 operands: 65
62	Literal
63	ExprTuple	66
64	Lambda	parameter: 185 body: 67
65	ExprTuple	179, 159
66	Operation	operator: 68 operands: 69
67	Operation	operator: 136 operands: 70
68	Literal
69	ExprTuple	71, 72, 73
70	ExprTuple	74, 75
71	ExprTuple	76, 77
72	ExprRange	lambda_map: 78 start_index: 176 end_index: 175
73	ExprTuple	79, 80
74	Operation	operator: 81 operands: 82
75	Operation	operator: 154 operands: 83
76	ExprRange	lambda_map: 84 start_index: 176 end_index: 175
77	ExprRange	lambda_map: 85 start_index: 176 end_index: 159
78	Lambda	parameter: 158 body: 86
79	ExprRange	lambda_map: 87 start_index: 176 end_index: 175
80	ExprRange	lambda_map: 88 start_index: 176 end_index: 159
81	Literal
82	ExprTuple	89, 123
83	ExprTuple	162, 123
84	Lambda	parameter: 185 body: 90
85	Lambda	parameter: 185 body: 91
86	ExprTuple	92, 93
87	Lambda	parameter: 185 body: 94
88	Lambda	parameter: 185 body: 95
89	IndexedVar	variable: 149 index: 185
90	Operation	operator: 109 operands: 96
91	Operation	operator: 134 operands: 97
92	ExprRange	lambda_map: 98 start_index: 176 end_index: 175
93	ExprRange	lambda_map: 99 start_index: 176 end_index: 159
94	Operation	operator: 114 operands: 100
95	Operation	operator: 134 operands: 101
96	NamedExprs	state: 102
97	NamedExprs	element: 103 targets: 120
98	Lambda	parameter: 185 body: 104
99	Lambda	parameter: 185 body: 105
100	NamedExprs	state: 106
101	NamedExprs	element: 107 targets: 120
102	Operation	operator: 169 operand: 116
103	Operation	operator: 109 operands: 115
104	Operation	operator: 110 operands: 111
105	Operation	operator: 134 operands: 112
106	Operation	operator: 154 operands: 113
107	Operation	operator: 114 operands: 115
108	ExprTuple	116
109	Literal
110	Literal
111	ExprTuple	117, 118
112	NamedExprs	element: 119 targets: 120
113	ExprTuple	121, 122
114	Literal
115	NamedExprs	state: 123 part: 185
116	Literal
117	Conditional	value: 124 condition: 125
118	Conditional	value: 126 condition: 127
119	Operation	operator: 137 operands: 128
120	Operation	operator: 129 operands: 130
121	Operation	operator: 165 operands: 131
122	Operation	operator: 132 operands: 133
123	Variable
124	Operation	operator: 134 operands: 135
125	Operation	operator: 136 operands: 140
126	Operation	operator: 137 operands: 138
127	Operation	operator: 139 operands: 140
128	NamedExprs	operation: 141 part: 185
129	Literal
130	ExprTuple	164, 142
131	ExprTuple	176, 143
132	Literal
133	ExprTuple	144, 145
134	Literal
135	NamedExprs	element: 146 targets: 147
136	Literal
137	Literal
138	NamedExprs	operation: 148
139	Literal
140	ExprTuple	158, 185
141	IndexedVar	variable: 149 index: 158
142	Operation	operator: 171 operands: 151
143	Operation	operator: 167 operands: 152
144	Operation	operator: 169 operand: 161
145	Operation	operator: 154 operands: 155
146	Literal
147	Operation	operator: 156 operand: 164
148	Literal
149	Variable
150	ExprTuple	158
151	ExprTuple	175, 159
152	ExprTuple	179, 160
153	ExprTuple	161
154	Literal
155	ExprTuple	162, 163
156	Literal
157	ExprTuple	164
158	Variable
159	Variable
160	Operation	operator: 165 operands: 166
161	Literal
162	Operation	operator: 167 operands: 168
163	Operation	operator: 169 operand: 176
164	Operation	operator: 171 operands: 172
165	Literal
166	ExprTuple	176, 179
167	Literal
168	ExprTuple	173, 174
169	Literal
170	ExprTuple	176
171	Literal
172	ExprTuple	175, 176
173	Literal
174	Operation	operator: 177 operands: 178
175	Variable
176	Literal
177	Literal
178	ExprTuple	179, 180, 181, 182
179	Literal
180	Literal
181	Literal
182	IndexedVar	variable: 183 index: 185
183	Variable
184	ExprTuple	185
185	Variable