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 Conditional, ExprTuple, Lambda, e
from proveit.logic import Equals, InSet
from proveit.physics.quantum.QPE import Pfail, _e_domain, _fail_prob_e

# build up the expression from sub-expressions
expr = ExprTuple(Lambda(e, Conditional(Equals(Pfail(e), _fail_prob_e), InSet(e, _e_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(e \mapsto \left\{\left[P_{\rm fail}\right]\left(e\right) = \left[\begin{array}{l}\textrm{Prob}_{m \in \{0~\ldotp \ldotp~2^{t} - 1\}~|~\left|m - b_{\textit{f}}\right|_{\textup{mod}\thinspace 2^{t}} > 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] \textrm{ if } e \in \{1~\ldotp \ldotp~2^{t - 1} - 2\}\right..\right)

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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