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 ExprRange, ExprTuple, Variable, VertExprArray, l
from proveit.numbers import Abs, Add, Exp, Interval, Sum, one, two
from proveit.physics.quantum import NumKet, Z, ket_plus
from proveit.physics.quantum.QPE import ModAdd, QPE, _U, _b_floor, _ket_u, _neg_domain, _rel_indexed_alpha, _s, _s_wire, _t
from proveit.physics.quantum.circuits import Gate, Input, Measure, MultiQubitElem, Output, Qcircuit
from proveit.statistics import ProbOfAll

# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = [l]
sub_expr3 = Add(_t, one)
sub_expr4 = Add(_t, _s)
sub_expr5 = Interval(sub_expr3, sub_expr4)
sub_expr6 = MultiQubitElem(element = Gate(operation = QPE(_U, _t), part = sub_expr1), targets = Interval(one, sub_expr4))
expr = ExprTuple(ProbOfAll(instance_param_or_params = sub_expr2, instance_element = Qcircuit(vert_expr_array = VertExprArray([ExprRange(sub_expr1, Input(state = ket_plus), one, _t), ExprRange(sub_expr1, MultiQubitElem(element = Input(state = _ket_u, part = sub_expr1), targets = sub_expr5), one, _s)], [ExprRange(sub_expr1, sub_expr6, one, _t), ExprRange(sub_expr1, sub_expr6, sub_expr3, sub_expr4)], [ExprRange(sub_expr1, Measure(basis = Z), one, _t), _s_wire], [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(ModAdd(_b_floor, l), _t), part = sub_expr1), targets = Interval(one, _t)), one, _t), ExprRange(sub_expr1, MultiQubitElem(element = Output(state = _ket_u, part = sub_expr1), targets = sub_expr5), one, _s)])), domain = _neg_domain), Sum(index_or_indices = sub_expr2, summand = Exp(Abs(_rel_indexed_alpha), two), domain = _neg_domain))

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(\textrm{Prob}_{l \in \{-2^{t - 1} + 1~\ldotp \ldotp~-\left(e + 1\right)\}}~\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \multigate{4}{\textrm{QPE}\left(U, t\right)} & \meter & \multiqout{3}{\lvert b_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert b_{\textit{f}} \oplus l \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 b_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert b_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right), \sum_{l = -2^{t - 1} + 1}^{-\left(e + 1\right)} \left|\alpha_{b_{\textit{f}} \oplus l}\right|^{2}\right)

stored_expr.style_options()

name	description	default	current value	related methods
wrap_positions	position(s) at which wrapping is to occur; 'n' is after the nth comma.	()	()	('with_wrapping_at',)
justification	if any wrap positions are set, justify to the 'left', 'center', or 'right'	left	left	('with_justification',)

# display the expression information
stored_expr.expr_info()

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