Expression of type Lambda

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, Lambda, 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 = Lambda(e, 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())

e \mapsto \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()

no style options

# display the expression information
stored_expr.expr_info()

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