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, U, Variable, VertExprArray, eps, m, n, s, t
from proveit.numbers import Add, Exp, Interval, LessEq, ModAbs, Neg, frac, one, 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 ProbOfAll

# 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(subtract(one, eps), ProbOfAll(instance_param_or_params = [m], instance_element = 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(m, 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)])), domain = Interval(zero, subtract(two_pow_t, one)), condition = LessEq(ModAbs(subtract(frac(m, two_pow_t), phase), one), Exp(two, Neg(n)))).with_wrapping())

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(1 - \epsilon, \begin{array}{l}\textrm{Prob}_{m \in \{0~\ldotp \ldotp~2^{t} - 1\}~|~\left|\frac{m}{2^{t}} - \varphi\right|_{\textup{mod}\thinspace 1} \leq 2^{-n}}~\\
\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \multigate{4}{\textrm{QPE}\left(U, t\right)} & \meter & \multiqout{3}{\lvert m \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert m \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 m \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert m \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right)\end{array}\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: 117 operands: 3
2	Operation	operator: 4 operand: 7
3	ExprTuple	123, 6
4	Literal
5	ExprTuple	7
6	Operation	operator: 110 operand: 11
7	Lambda	parameter: 122 body: 10
8	ExprTuple	11
9	ExprTuple	122
10	Conditional	value: 12 condition: 13
11	Variable
12	Operation	operator: 14 operands: 15
13	Operation	operator: 16 operands: 17
14	Literal
15	ExprTuple	18, 19, 20, 21
16	Literal
17	ExprTuple	22, 23
18	ExprTuple	24, 25
19	ExprTuple	26, 27
20	ExprTuple	28, 29
21	ExprTuple	30, 31
22	Operation	operator: 32 operands: 33
23	Operation	operator: 34 operands: 35
24	ExprRange	lambda_map: 36 start_index: 123 end_index: 128
25	ExprRange	lambda_map: 37 start_index: 123 end_index: 124
26	ExprRange	lambda_map: 38 start_index: 123 end_index: 128
27	ExprRange	lambda_map: 38 start_index: 105 end_index: 106
28	ExprRange	lambda_map: 39 start_index: 123 end_index: 128
29	ExprRange	lambda_map: 40 start_index: 123 end_index: 124
30	ExprRange	lambda_map: 41 start_index: 123 end_index: 128
31	ExprRange	lambda_map: 42 start_index: 123 end_index: 124
32	Literal
33	ExprTuple	122, 43
34	Literal
35	ExprTuple	44, 45
36	Lambda	parameter: 104 body: 46
37	Lambda	parameter: 104 body: 47
38	Lambda	parameter: 104 body: 48
39	Lambda	parameter: 104 body: 49
40	Lambda	parameter: 104 body: 50
41	Lambda	parameter: 104 body: 51
42	Lambda	parameter: 104 body: 53
43	Operation	operator: 94 operands: 54
44	Operation	operator: 55 operands: 56
45	Operation	operator: 125 operands: 57
46	Operation	operator: 86 operands: 58
47	Operation	operator: 65 operands: 59
48	Operation	operator: 65 operands: 60
49	Operation	operator: 61 operands: 62
50	Operation	operator: 87 operands: 63
51	Operation	operator: 65 operands: 64
52	ExprTuple	104
53	Operation	operator: 65 operands: 66
54	ExprTuple	67, 68
55	Literal
56	ExprTuple	69, 123
57	ExprTuple	127, 70
58	NamedExprs	state: 71
59	NamedExprs	element: 72 targets: 80
60	NamedExprs	element: 73 targets: 74
61	Literal
62	NamedExprs	basis: 75
63	NamedExprs	operation: 76
64	NamedExprs	element: 77 targets: 78
65	Literal
66	NamedExprs	element: 79 targets: 80
67	Literal
68	Operation	operator: 117 operands: 81
69	Operation	operator: 117 operands: 82
70	Operation	operator: 110 operand: 99
71	Operation	operator: 84 operand: 100
72	Operation	operator: 86 operands: 93
73	Operation	operator: 87 operands: 88
74	Operation	operator: 94 operands: 89
75	Literal
76	Literal
77	Operation	operator: 92 operands: 90
78	Operation	operator: 94 operands: 91
79	Operation	operator: 92 operands: 93
80	Operation	operator: 94 operands: 95
81	ExprTuple	119, 96
82	ExprTuple	97, 98
83	ExprTuple	99
84	Literal
85	ExprTuple	100
86	Literal
87	Literal
88	NamedExprs	operation: 101 part: 104
89	ExprTuple	123, 106
90	NamedExprs	state: 102 part: 104
91	ExprTuple	123, 128
92	Literal
93	NamedExprs	state: 103 part: 104
94	Literal
95	ExprTuple	105, 106
96	Operation	operator: 110 operand: 123
97	Operation	operator: 108 operands: 109
98	Operation	operator: 110 operand: 120
99	Variable
100	Literal
101	Operation	operator: 112 operands: 113
102	Operation	operator: 114 operands: 115
103	Variable
104	Variable
105	Operation	operator: 117 operands: 116
106	Operation	operator: 117 operands: 118
107	ExprTuple	123
108	Literal
109	ExprTuple	122, 119
110	Literal
111	ExprTuple	120
112	Literal
113	ExprTuple	121, 128
114	Literal
115	ExprTuple	122, 128
116	ExprTuple	128, 123
117	Literal
118	ExprTuple	128, 124
119	Operation	operator: 125 operands: 126
120	Variable
121	Variable
122	Variable
123	Literal
124	Variable
125	Literal
126	ExprTuple	127, 128
127	Literal
128	Variable