Expression of type ExprTuple

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 Conditional, ExprRange, ExprTuple, Lambda, U, Variable, VertExprArray, s, t
from proveit.linear_algebra import MatrixMult, ScalarMult, Unitary
from proveit.logic import And, Equals, Forall, InSet
from proveit.numbers import Add, Exp, Interval, IntervalCO, Mod, Mult, NaturalPos, Real, Round, e, four, frac, greater, i, one, pi, 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 = 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 = ExprTuple(Lambda([s, t], Conditional(Forall(instance_param_or_params = [U], instance_expr = Forall(instance_param_or_params = [var_ket_u], instance_expr = Forall(instance_param_or_params = [phase], instance_expr = greater(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_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(Mod(Round(Mult(two_pow_t, phase)), two_pow_t), 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)]))), frac(four, Exp(pi, two))), domain = Real, conditions = [InSet(phase, IntervalCO(zero, one)), Equals(MatrixMult(U, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, phase)), var_ket_u))]).with_wrapping(), domain = s_ket_domain, condition = normalized_var_ket_u).with_wrapping(), domain = Unitary(two_pow_s)).with_wrapping(), And(InSet(s, 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(\left(s, t\right) \mapsto \left\{\begin{array}{l}\forall_{U \in \textrm{U}\left(2^{s}\right)}~\\
\left[\begin{array}{l}\forall_{\lvert u \rangle \in \mathbb{C}^{2^{s}}~|~\left \|\lvert u \rangle\right \| = 1}~\\
\left[\begin{array}{l}\forall_{\varphi \in \mathbb{R}~|~\varphi \in \left[0,1\right), \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 round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \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 round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right) > \frac{4}{\pi^{2}}\right)\end{array}\right]\end{array}\right]\end{array} \textrm{ if } s \in \mathbb{N}^+ ,  t \in \mathbb{N}^+\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	165, 179
3	Conditional	value: 4 condition: 5
4	Operation	operator: 27 operand: 8
5	Operation	operator: 43 operands: 7
6	ExprTuple	8
7	ExprTuple	9, 10
8	Lambda	parameter: 162 body: 12
9	Operation	operator: 61 operands: 13
10	Operation	operator: 61 operands: 14
11	ExprTuple	162
12	Conditional	value: 15 condition: 16
13	ExprTuple	165, 17
14	ExprTuple	179, 17
15	Operation	operator: 27 operand: 20
16	Operation	operator: 61 operands: 19
17	Literal
18	ExprTuple	20
19	ExprTuple	162, 21
20	Lambda	parameter: 151 body: 22
21	Operation	operator: 23 operand: 55
22	Conditional	value: 25 condition: 26
23	Literal
24	ExprTuple	55
25	Operation	operator: 27 operand: 30
26	Operation	operator: 43 operands: 29
27	Literal
28	ExprTuple	30
29	ExprTuple	31, 32
30	Lambda	parameter: 175 body: 34
31	Operation	operator: 61 operands: 35
32	Operation	operator: 63 operands: 36
33	ExprTuple	175
34	Conditional	value: 37 condition: 38
35	ExprTuple	151, 39
36	ExprTuple	40, 164
37	Operation	operator: 41 operands: 42
38	Operation	operator: 43 operands: 44
39	Operation	operator: 45 operands: 46
40	Operation	operator: 47 operand: 151
41	Literal
42	ExprTuple	49, 50
43	Literal
44	ExprTuple	51, 52, 53
45	Literal
46	ExprTuple	54, 55
47	Literal
48	ExprTuple	151
49	Operation	operator: 56 operands: 57
50	Operation	operator: 58 operand: 68
51	Operation	operator: 61 operands: 60
52	Operation	operator: 61 operands: 62
53	Operation	operator: 63 operands: 64
54	Literal
55	Operation	operator: 176 operands: 65
56	Literal
57	ExprTuple	66, 67
58	Literal
59	ExprTuple	68
60	ExprTuple	175, 69
61	Literal
62	ExprTuple	175, 70
63	Literal
64	ExprTuple	71, 72
65	ExprTuple	178, 165
66	Literal
67	Operation	operator: 176 operands: 73
68	Operation	operator: 74 operands: 75
69	Literal
70	Operation	operator: 76 operands: 77
71	Operation	operator: 78 operands: 79
72	Operation	operator: 80 operands: 81
73	ExprTuple	124, 178
74	Literal
75	ExprTuple	82, 83, 84, 85
76	Literal
77	ExprTuple	86, 164
78	Literal
79	ExprTuple	162, 151
80	Literal
81	ExprTuple	87, 151
82	ExprTuple	88, 89
83	ExprTuple	90, 91
84	ExprTuple	92, 93
85	ExprTuple	94, 95
86	Literal
87	Operation	operator: 176 operands: 96
88	ExprRange	lambda_map: 97 start_index: 164 end_index: 179
89	ExprRange	lambda_map: 98 start_index: 164 end_index: 165
90	ExprRange	lambda_map: 99 start_index: 164 end_index: 179
91	ExprRange	lambda_map: 99 start_index: 153 end_index: 154
92	ExprRange	lambda_map: 100 start_index: 164 end_index: 179
93	ExprRange	lambda_map: 101 start_index: 164 end_index: 165
94	ExprRange	lambda_map: 102 start_index: 164 end_index: 179
95	ExprRange	lambda_map: 103 start_index: 164 end_index: 165
96	ExprTuple	104, 105
97	Lambda	parameter: 152 body: 106
98	Lambda	parameter: 152 body: 107
99	Lambda	parameter: 152 body: 108
100	Lambda	parameter: 152 body: 109
101	Lambda	parameter: 152 body: 110
102	Lambda	parameter: 152 body: 111
103	Lambda	parameter: 152 body: 113
104	Literal
105	Operation	operator: 172 operands: 114
106	Operation	operator: 138 operands: 115
107	Operation	operator: 122 operands: 116
108	Operation	operator: 122 operands: 117
109	Operation	operator: 118 operands: 119
110	Operation	operator: 139 operands: 120
111	Operation	operator: 122 operands: 121
112	ExprTuple	152
113	Operation	operator: 122 operands: 123
114	ExprTuple	178, 124, 125, 175
115	NamedExprs	state: 126
116	NamedExprs	element: 127 targets: 135
117	NamedExprs	element: 128 targets: 129
118	Literal
119	NamedExprs	basis: 130
120	NamedExprs	operation: 131
121	NamedExprs	element: 132 targets: 133
122	Literal
123	NamedExprs	element: 134 targets: 135
124	Literal
125	Literal
126	Operation	operator: 136 operand: 148
127	Operation	operator: 138 operands: 145
128	Operation	operator: 139 operands: 140
129	Operation	operator: 146 operands: 141
130	Literal
131	Literal
132	Operation	operator: 144 operands: 142
133	Operation	operator: 146 operands: 143
134	Operation	operator: 144 operands: 145
135	Operation	operator: 146 operands: 147
136	Literal
137	ExprTuple	148
138	Literal
139	Literal
140	NamedExprs	operation: 149 part: 152
141	ExprTuple	164, 154
142	NamedExprs	state: 150 part: 152
143	ExprTuple	164, 179
144	Literal
145	NamedExprs	state: 151 part: 152
146	Literal
147	ExprTuple	153, 154
148	Literal
149	Operation	operator: 155 operands: 156
150	Operation	operator: 157 operands: 158
151	Variable
152	Variable
153	Operation	operator: 160 operands: 159
154	Operation	operator: 160 operands: 161
155	Literal
156	ExprTuple	162, 179
157	Literal
158	ExprTuple	163, 179
159	ExprTuple	179, 164
160	Literal
161	ExprTuple	179, 165
162	Variable
163	Operation	operator: 166 operands: 167
164	Literal
165	Variable
166	Literal
167	ExprTuple	168, 174
168	Operation	operator: 169 operand: 171
169	Literal
170	ExprTuple	171
171	Operation	operator: 172 operands: 173
172	Literal
173	ExprTuple	174, 175
174	Operation	operator: 176 operands: 177
175	Variable
176	Literal
177	ExprTuple	178, 179
178	Literal
179	Variable