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, Mult, Real, e, i, one, pi, subtract, 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 = 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(phase, Conditional(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), And(InSet(phase, Real), 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)), InSet(phase, IntervalCO(zero, one))))))

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