Expression of type Equals ¶

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 ExprRange, Variable, VertExprArray, e, l, m
from proveit.logic import Equals
from proveit.numbers import Add, Interval, ModAbs, greater, one, subtract
from proveit.physics.quantum import NumKet, Z, ket_plus
from proveit.physics.quantum.QPE import ModAdd, QPE, _U, _b_floor, _full_domain, _ket_u, _m_domain, _phase_est_circuit, _s, _s_wire, _t, _two_pow_t
from proveit.physics.quantum.circuits import Gate, Input, Measure, MultiQubitElem, Output, Qcircuit
from proveit.statistics import ProbOfAll

# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = Add(_t, one)
sub_expr3 = Add(_t, _s)
sub_expr4 = Interval(sub_expr2, sub_expr3)
sub_expr5 = MultiQubitElem(element = Gate(operation = QPE(_U, _t), part = sub_expr1), targets = Interval(one, sub_expr3))
expr = Equals(ProbOfAll(instance_param_or_params = [m], instance_element = _phase_est_circuit, domain = _m_domain, condition = greater(ModAbs(subtract(m, _b_floor), _two_pow_t), e)), ProbOfAll(instance_param_or_params = [l], instance_element = Qcircuit(vert_expr_array = VertExprArray([ExprRange(sub_expr1, Input(state = ket_plus), one, _t), ExprRange(sub_expr1, MultiQubitElem(element = Input(state = _ket_u, part = sub_expr1), targets = sub_expr4), one, _s)], [ExprRange(sub_expr1, sub_expr5, one, _t), ExprRange(sub_expr1, sub_expr5, sub_expr2, sub_expr3)], [ExprRange(sub_expr1, Measure(basis = Z), one, _t), _s_wire], [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(ModAdd(_b_floor, l), _t), part = sub_expr1), targets = Interval(one, _t)), one, _t), ExprRange(sub_expr1, MultiQubitElem(element = Output(state = _ket_u, part = sub_expr1), targets = sub_expr4), one, _s)])), domain = _full_domain, condition = greater(ModAbs(l, _two_pow_t), e)))

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

\left[\textrm{Prob}_{m \in \{0~\ldotp \ldotp~2^{t} - 1\}~|~\left|m - b_{\textit{f}}\right|_{\textup{mod}\thinspace 2^{t}} > 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)\right] = \left[\textrm{Prob}_{l \in \{-2^{t - 1} + 1~\ldotp \ldotp~2^{t - 1}\}~|~\left|l\right|_{\textup{mod}\thinspace 2^{t}} > 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 b_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert b_{\textit{f}} \oplus l \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 b_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert b_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right)\right]

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

Expression of type Equals¶

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

Expression of type Equals ¶

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