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