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
from proveit.logic import And, Equals, Forall, InSet
from proveit.numbers import Add, Exp, Interval, IntervalCO, Mod, Mult, 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_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(var_ket_u, Conditional(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(), And(InSet(var_ket_u, s_ket_domain), normalized_var_ket_u))))

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