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 Equals, Forall, InSet
from proveit.numbers import Add, Exp, Interval, Mult, 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(U, Conditional(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(), InSet(U, Unitary(two_pow_s)))))

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