Expression of type ExprTuple

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, ExprTuple, IndexedVar, Lambda, 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, 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 = ExprTuple(Lambda([ExprRange(sub_expr1, sub_expr2, one, t)], Conditional(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(), And(ExprRange(sub_expr1, InSet(sub_expr2, Unitary(Exp(two, m))), one, t)))))

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(\left(U_{1}, U_{2}, \ldots, U_{t}\right) \mapsto \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} \textrm{ if } \left(U_{1} \in \textrm{U}\left(2^{m}\right)\right) \land  \left(U_{2} \in \textrm{U}\left(2^{m}\right)\right) \land  \ldots \land  \left(U_{t} \in \textrm{U}\left(2^{m}\right)\right)\right..\right)

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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