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
from proveit.physics.quantum.QPE import Psuccess, _success_prob_e

# build up the expression from sub-expressions
expr = ExprTuple(Psuccess(e), _success_prob_e)

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