Expression of type Implies ¶

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.logic import Forall, Implies
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]
sub_expr2 = LessEq(ModAbs(subtract(m, _b_floor), _two_pow_t), _e_value)
expr = Implies(Forall(instance_param_or_params = sub_expr1, instance_expr = _success_cond, domain = _m_domain, condition = sub_expr2), LessEq(ProbOfAll(instance_param_or_params = sub_expr1, instance_element = _phase_est_circuit, domain = _m_domain, condition = sub_expr2), ProbOfAll(instance_param_or_params = sub_expr1, instance_element = _phase_est_circuit, domain = _m_domain, condition = _success_cond)).with_wrapping_at(2)).with_wrapping_at(2)

# 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[\forall_{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(\left|\frac{m}{2^{t}} - \varphi\right|_{\textup{mod}\thinspace 1} \leq 2^{-n}\right)\right] \Rightarrow  \\ \left(\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}\right) \end{array} \end{array}

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

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

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

Expression of type Implies¶

from the theory of proveit.physics.quantum.QPE¶

Expression of type Implies ¶

from the theory of proveit.physics.quantum.QPE ¶