Expression of type Conditional

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 Conditional, ExprRange, IndexedVar, U, Variable, m, t
from proveit.linear_algebra import MatrixMult, ScalarMult, Unitary
from proveit.logic import And, Equals, Forall, InSet
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 = Conditional(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(), And(InSet(m, 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\{\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} \textrm{ if } m \in \mathbb{N}^+ ,  t \in \mathbb{N}^+\right..

stored_expr.style_options()

name	description	default	current value	related methods
condition_delimiter	'comma' or 'and'	comma	comma	('with_comma_delimiter', 'with_conjunction_delimiter')

# display the expression information
stored_expr.expr_info()

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