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