Theorem _precision_guarantee of type LessEq

from the theory of proveit.physics.quantum.QPE

see dependencies

import proveit
# Automation is not needed when only building an expression:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%load_theorem_expr # Load the stored theorem expression as 'stored_expr'
# import the special expression
from proveit.physics.quantum.QPE import _precision_guarantee

# check that the built expression is the same as the stored expression
assert _precision_guarantee.expr == stored_expr
assert _precision_guarantee.expr._style_id == stored_expr._style_id
print("Passed sanity check: _precision_guarantee matches stored_expr")

Passed sanity check: _precision_guarantee matches stored_expr

# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())

\left[\begin{array}{l}\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)\end{array}\right] \geq \left(1 - \epsilon\right)

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.	()	()	('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	reversed	('with_direction_reversed', 'is_reversed')

# display the expression information
stored_expr.expr_info()

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