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