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, m
from proveit.logic import And, InSet
from proveit.physics.quantum.QPE import _m_domain, _phase_est_circuit, _success_cond

# build up the expression from sub-expressions
expr = Lambda(m, Conditional(_phase_est_circuit, And(InSet(m, _m_domain), _success_cond)))

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())

m \mapsto \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} \textrm{ if } m \in \{0~\ldotp \ldotp~2^{t} - 1\} ,  \left|\frac{m}{2^{t}} - \varphi\right|_{\textup{mod}\thinspace 1} \leq 2^{-n}\right..

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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