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