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 Add, Interval, one
from proveit.physics.quantum import NumKet, Z, ket_plus
from proveit.physics.quantum.QPE import ModAdd, QPE, _U, _b_floor, _ket_u, _neg_domain, _pos_domain, _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))
sub_expr7 = 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)]))
expr = ExprTuple(ProbOfAll(instance_param_or_params = sub_expr2, instance_element = sub_expr7, domain = _neg_domain), ProbOfAll(instance_param_or_params = sub_expr2, instance_element = sub_expr7, domain = _pos_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), \textrm{Prob}_{l \in \{e + 1~\ldotp \ldotp~2^{t - 1}\}}~\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)\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: 4 operand: 6
2	Operation	operator: 4 operand: 7
3	ExprTuple	6
4	Literal
5	ExprTuple	7
6	Lambda	parameter: 120 body: 8
7	Lambda	parameter: 120 body: 10
8	Conditional	value: 12 condition: 11
9	ExprTuple	120
10	Conditional	value: 12 condition: 13
11	Operation	operator: 17 operands: 14
12	Operation	operator: 15 operands: 16
13	Operation	operator: 17 operands: 18
14	ExprTuple	120, 19
15	Literal
16	ExprTuple	20, 21, 22, 23
17	Literal
18	ExprTuple	120, 24
19	Operation	operator: 89 operands: 25
20	ExprTuple	26, 27
21	ExprTuple	28, 29
22	ExprTuple	30, 31
23	ExprTuple	32, 33
24	Operation	operator: 89 operands: 34
25	ExprTuple	35, 36
26	ExprRange	lambda_map: 37 start_index: 121 end_index: 113
27	ExprRange	lambda_map: 38 start_index: 121 end_index: 112
28	ExprRange	lambda_map: 39 start_index: 121 end_index: 113
29	ExprRange	lambda_map: 39 start_index: 98 end_index: 99
30	ExprRange	lambda_map: 40 start_index: 121 end_index: 113
31	ExprRange	lambda_map: 41 start_index: 121 end_index: 112
32	ExprRange	lambda_map: 42 start_index: 121 end_index: 113
33	ExprRange	lambda_map: 43 start_index: 121 end_index: 112
34	ExprTuple	55, 77
35	Operation	operator: 108 operands: 44
36	Operation	operator: 117 operand: 55
37	Lambda	parameter: 97 body: 46
38	Lambda	parameter: 97 body: 47
39	Lambda	parameter: 97 body: 48
40	Lambda	parameter: 97 body: 49
41	Lambda	parameter: 97 body: 50
42	Lambda	parameter: 97 body: 51
43	Lambda	parameter: 97 body: 53
44	ExprTuple	54, 121
45	ExprTuple	55
46	Operation	operator: 81 operands: 56
47	Operation	operator: 63 operands: 57
48	Operation	operator: 63 operands: 58
49	Operation	operator: 59 operands: 60
50	Operation	operator: 82 operands: 61
51	Operation	operator: 63 operands: 62
52	ExprTuple	97
53	Operation	operator: 63 operands: 64
54	Operation	operator: 117 operand: 77
55	Operation	operator: 108 operands: 66
56	NamedExprs	state: 67
57	NamedExprs	element: 68 targets: 76
58	NamedExprs	element: 69 targets: 70
59	Literal
60	NamedExprs	basis: 71
61	NamedExprs	operation: 72
62	NamedExprs	element: 73 targets: 74
63	Literal
64	NamedExprs	element: 75 targets: 76
65	ExprTuple	77
66	ExprTuple	78, 121
67	Operation	operator: 79 operand: 93
68	Operation	operator: 81 operands: 88
69	Operation	operator: 82 operands: 83
70	Operation	operator: 89 operands: 84
71	Literal
72	Literal
73	Operation	operator: 87 operands: 85
74	Operation	operator: 89 operands: 86
75	Operation	operator: 87 operands: 88
76	Operation	operator: 89 operands: 90
77	Operation	operator: 91 operands: 92
78	Variable
79	Literal
80	ExprTuple	93
81	Literal
82	Literal
83	NamedExprs	operation: 94 part: 97
84	ExprTuple	121, 99
85	NamedExprs	state: 95 part: 97
86	ExprTuple	121, 113
87	Literal
88	NamedExprs	state: 96 part: 97
89	Literal
90	ExprTuple	98, 99
91	Literal
92	ExprTuple	100, 101
93	Literal
94	Operation	operator: 102 operands: 103
95	Operation	operator: 104 operands: 105
96	Literal
97	Variable
98	Operation	operator: 108 operands: 106
99	Operation	operator: 108 operands: 107
100	Literal
101	Operation	operator: 108 operands: 109
102	Literal
103	ExprTuple	110, 113
104	Literal
105	ExprTuple	111, 113
106	ExprTuple	113, 121
107	ExprTuple	113, 112
108	Literal
109	ExprTuple	113, 114
110	Literal
111	Operation	operator: 115 operands: 116
112	Literal
113	Literal
114	Operation	operator: 117 operand: 121
115	Literal
116	ExprTuple	119, 120
117	Literal
118	ExprTuple	121
119	Literal
120	Variable
121	Literal