Expression of type Conditional

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, e
from proveit.logic import Equals, InSet
from proveit.physics.quantum.QPE import Psuccess, _e_domain, _success_prob_e

# build up the expression from sub-expressions
expr = Conditional(Equals(Psuccess(e), _success_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\{\left[P_{\rm success}\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}} \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] \textrm{ if } e \in \{1~\ldotp \ldotp~2^{t - 1} - 2\}\right..

stored_expr.style_options()

name	description	default	current value	related methods
condition_delimiter	'comma' or 'and'	comma	comma	('with_comma_delimiter', 'with_conjunction_delimiter')

# display the expression information
stored_expr.expr_info()

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