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 ExprTuple, e, m
from proveit.logic import SetOfAll
from proveit.numbers import ModAbs, greater, subtract
from proveit.physics.quantum.QPE import _b_floor, _m_domain, _phase_est_circuit, _sample_space, _two_pow_t

# build up the expression from sub-expressions
expr = ExprTuple(SetOfAll(instance_param_or_params = [m], instance_element = _phase_est_circuit, domain = _m_domain, condition = greater(ModAbs(subtract(m, _b_floor), _two_pow_t), e)), _sample_space)

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(\left\{\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)~|~\left|m - b_{\textit{f}}\right|_{\textup{mod}\thinspace 2^{t}} > e\right\}_{m \in \{0~\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 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\}_{m \in \{0~\ldotp \ldotp~2^{t} - 1\}}\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: 117 body: 8
7	Lambda	parameter: 117 body: 10
8	Conditional	value: 12 condition: 11
9	ExprTuple	117
10	Conditional	value: 12 condition: 17
11	Operation	operator: 13 operands: 14
12	Operation	operator: 15 operands: 16
13	Literal
14	ExprTuple	17, 18
15	Literal
16	ExprTuple	19, 20, 21, 22
17	Operation	operator: 23 operands: 24
18	Operation	operator: 25 operands: 26
19	ExprTuple	27, 28
20	ExprTuple	29, 30
21	ExprTuple	31, 32
22	ExprTuple	33, 34
23	Literal
24	ExprTuple	117, 35
25	Literal
26	ExprTuple	36, 37
27	ExprRange	lambda_map: 38 start_index: 118 end_index: 119
28	ExprRange	lambda_map: 39 start_index: 118 end_index: 120
29	ExprRange	lambda_map: 40 start_index: 118 end_index: 119
30	ExprRange	lambda_map: 40 start_index: 105 end_index: 106
31	ExprRange	lambda_map: 41 start_index: 118 end_index: 119
32	ExprRange	lambda_map: 42 start_index: 118 end_index: 120
33	ExprRange	lambda_map: 43 start_index: 118 end_index: 119
34	ExprRange	lambda_map: 44 start_index: 118 end_index: 120
35	Operation	operator: 93 operands: 45
36	Variable
37	Operation	operator: 46 operands: 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: 52
43	Lambda	parameter: 104 body: 53
44	Lambda	parameter: 104 body: 55
45	ExprTuple	56, 57
46	Literal
47	ExprTuple	58, 80
48	Operation	operator: 85 operands: 59
49	Operation	operator: 66 operands: 60
50	Operation	operator: 66 operands: 61
51	Operation	operator: 62 operands: 63
52	Operation	operator: 86 operands: 64
53	Operation	operator: 66 operands: 65
54	ExprTuple	104
55	Operation	operator: 66 operands: 67
56	Literal
57	Operation	operator: 114 operands: 68
58	Operation	operator: 114 operands: 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	ExprTuple	80, 81
69	ExprTuple	117, 82
70	Operation	operator: 83 operand: 100
71	Operation	operator: 85 operands: 92
72	Operation	operator: 86 operands: 87
73	Operation	operator: 93 operands: 88
74	Literal
75	Literal
76	Operation	operator: 91 operands: 89
77	Operation	operator: 93 operands: 90
78	Operation	operator: 91 operands: 92
79	Operation	operator: 93 operands: 94
80	Operation	operator: 95 operands: 96
81	Operation	operator: 98 operand: 118
82	Operation	operator: 98 operand: 108
83	Literal
84	ExprTuple	100
85	Literal
86	Literal
87	NamedExprs	operation: 101 part: 104
88	ExprTuple	118, 106
89	NamedExprs	state: 102 part: 104
90	ExprTuple	118, 119
91	Literal
92	NamedExprs	state: 103 part: 104
93	Literal
94	ExprTuple	105, 106
95	Literal
96	ExprTuple	107, 119
97	ExprTuple	118
98	Literal
99	ExprTuple	108
100	Literal
101	Operation	operator: 109 operands: 110
102	Operation	operator: 111 operands: 112
103	Literal
104	Variable
105	Operation	operator: 114 operands: 113
106	Operation	operator: 114 operands: 115
107	Literal
108	Literal
109	Literal
110	ExprTuple	116, 119
111	Literal
112	ExprTuple	117, 119
113	ExprTuple	119, 118
114	Literal
115	ExprTuple	119, 120
116	Literal
117	Variable
118	Literal
119	Literal
120	Literal