Expression of type LessEq

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 m
from proveit.numbers import LessEq, ModAbs, subtract
from proveit.physics.quantum.QPE import _b_floor, _e_value, _m_domain, _phase_est_circuit, _success_cond, _two_pow_t
from proveit.statistics import ProbOfAll

# build up the expression from sub-expressions
sub_expr1 = [m]
expr = LessEq(ProbOfAll(instance_param_or_params = sub_expr1, instance_element = _phase_est_circuit, domain = _m_domain, condition = LessEq(ModAbs(subtract(m, _b_floor), _two_pow_t), _e_value)), ProbOfAll(instance_param_or_params = sub_expr1, instance_element = _phase_est_circuit, domain = _m_domain, condition = _success_cond)).with_wrapping_at(2)

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

\begin{array}{c} \begin{array}{l} \left[\textrm{Prob}_{m \in \{0~\ldotp \ldotp~2^{t} - 1\}~|~\left|m - b_{\textit{f}}\right|_{\textup{mod}\thinspace 2^{t}} \leq \left(2^{t - n} - 1\right)}~\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)\right] \leq  \\ \left[\textrm{Prob}_{m \in \{0~\ldotp \ldotp~2^{t} - 1\}~|~\left|\frac{m}{2^{t}} - \varphi\right|_{\textup{mod}\thinspace 1} \leq 2^{-n}}~\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)\right] \end{array} \end{array}

stored_expr.style_options()

name	description	default	current value	related methods
operation	'infix' or 'function' style formatting	infix	infix
wrap_positions	position(s) at which wrapping is to occur; '2 n - 1' is after the nth operand, '2 n' is after the nth operation.	()	(2)	('with_wrapping_at', 'with_wrap_before_operator', 'with_wrap_after_operator', 'without_wrapping', 'wrap_positions')
justification	if any wrap positions are set, justify to the 'left', 'center', or 'right'	center	center	('with_justification',)
direction	Direction of the relation (normal or reversed)	normal	normal	('with_direction_reversed', 'is_reversed')

# display the expression information
stored_expr.expr_info()

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