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
from proveit.logic import Equals
from proveit.numbers import Abs, Add, Exp, Interval, ModAbs, Sum, greater, one, two
from proveit.physics.quantum import NumKet, Z, ket_plus
from proveit.physics.quantum.QPE import ModAdd, QPE, _U, _b_floor, _full_domain, _ket_u, _neg_domain, _pos_domain, _rel_indexed_alpha, _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 = [l]
sub_expr3 = Add(_t, one)
sub_expr4 = Add(_t, _s)
sub_expr5 = Interval(sub_expr3, sub_expr4)
sub_expr6 = MultiQubitElem(element = Gate(operation = QPE(_U, _t), part = sub_expr1), targets = Interval(one, sub_expr4))
sub_expr7 = Exp(Abs(_rel_indexed_alpha), two)
expr = Equals(ProbOfAll(instance_param_or_params = sub_expr2, 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_expr5), one, _s)], [ExprRange(sub_expr1, sub_expr6, one, _t), ExprRange(sub_expr1, sub_expr6, sub_expr3, sub_expr4)], [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_expr5), one, _s)])), domain = _full_domain, condition = greater(ModAbs(l, _two_pow_t), e)), Add(Sum(index_or_indices = sub_expr2, summand = sub_expr7, domain = _neg_domain), Sum(index_or_indices = sub_expr2, summand = sub_expr7, domain = _pos_domain))).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[\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] =  \\ \left(\left(\sum_{l = -2^{t - 1} + 1}^{-\left(e + 1\right)} \left|\alpha_{b_{\textit{f}} \oplus l}\right|^{2}\right) + \left(\sum_{l = e + 1}^{2^{t - 1}} \left|\alpha_{b_{\textit{f}} \oplus l}\right|^{2}\right)\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: 147 operands: 7
5	Literal
6	ExprTuple	8
7	ExprTuple	9, 10
8	Lambda	parameter: 146 body: 11
9	Operation	operator: 13 operand: 17
10	Operation	operator: 13 operand: 18
11	Conditional	value: 15 condition: 16
12	ExprTuple	17
13	Literal
14	ExprTuple	18
15	Operation	operator: 19 operands: 20
16	Operation	operator: 21 operands: 22
17	Lambda	parameter: 146 body: 23
18	Lambda	parameter: 146 body: 25
19	Literal
20	ExprTuple	26, 27, 28, 29
21	Literal
22	ExprTuple	30, 31
23	Conditional	value: 33 condition: 32
24	ExprTuple	146
25	Conditional	value: 33 condition: 34
26	ExprTuple	35, 36
27	ExprTuple	37, 38
28	ExprTuple	39, 40
29	ExprTuple	41, 42
30	Operation	operator: 48 operands: 43
31	Operation	operator: 44 operands: 45
32	Operation	operator: 48 operands: 46
33	Operation	operator: 139 operands: 47
34	Operation	operator: 48 operands: 49
35	ExprRange	lambda_map: 50 start_index: 153 end_index: 149
36	ExprRange	lambda_map: 51 start_index: 153 end_index: 138
37	ExprRange	lambda_map: 52 start_index: 153 end_index: 149
38	ExprRange	lambda_map: 52 start_index: 124 end_index: 125
39	ExprRange	lambda_map: 53 start_index: 153 end_index: 149
40	ExprRange	lambda_map: 54 start_index: 153 end_index: 138
41	ExprRange	lambda_map: 55 start_index: 153 end_index: 149
42	ExprRange	lambda_map: 56 start_index: 153 end_index: 138
43	ExprTuple	146, 57
44	Literal
45	ExprTuple	135, 58
46	ExprTuple	146, 59
47	ExprTuple	60, 143
48	Literal
49	ExprTuple	146, 61
50	Lambda	parameter: 123 body: 62
51	Lambda	parameter: 123 body: 63
52	Lambda	parameter: 123 body: 64
53	Lambda	parameter: 123 body: 65
54	Lambda	parameter: 123 body: 66
55	Lambda	parameter: 123 body: 67
56	Lambda	parameter: 123 body: 69
57	Operation	operator: 115 operands: 70
58	Operation	operator: 71 operands: 72
59	Operation	operator: 115 operands: 73
60	Operation	operator: 74 operand: 89
61	Operation	operator: 115 operands: 76
62	Operation	operator: 107 operands: 77
63	Operation	operator: 84 operands: 78
64	Operation	operator: 84 operands: 79
65	Operation	operator: 80 operands: 81
66	Operation	operator: 108 operands: 82
67	Operation	operator: 84 operands: 83
68	ExprTuple	123
69	Operation	operator: 84 operands: 85
70	ExprTuple	87, 134
71	Literal
72	ExprTuple	146, 86
73	ExprTuple	87, 88
74	Literal
75	ExprTuple	89
76	ExprTuple	118, 134
77	NamedExprs	state: 90
78	NamedExprs	element: 91 targets: 99
79	NamedExprs	element: 92 targets: 93
80	Literal
81	NamedExprs	basis: 94
82	NamedExprs	operation: 95
83	NamedExprs	element: 96 targets: 97
84	Literal
85	NamedExprs	element: 98 targets: 99
86	Operation	operator: 139 operands: 100
87	Operation	operator: 147 operands: 101
88	Operation	operator: 151 operand: 118
89	Operation	operator: 103 operand: 137
90	Operation	operator: 105 operand: 119
91	Operation	operator: 107 operands: 114
92	Operation	operator: 108 operands: 109
93	Operation	operator: 115 operands: 110
94	Literal
95	Literal
96	Operation	operator: 113 operands: 111
97	Operation	operator: 115 operands: 112
98	Operation	operator: 113 operands: 114
99	Operation	operator: 115 operands: 116
100	ExprTuple	143, 149
101	ExprTuple	117, 153
102	ExprTuple	118
103	Literal
104	ExprTuple	137
105	Literal
106	ExprTuple	119
107	Literal
108	Literal
109	NamedExprs	operation: 120 part: 123
110	ExprTuple	153, 125
111	NamedExprs	state: 121 part: 123
112	ExprTuple	153, 149
113	Literal
114	NamedExprs	state: 122 part: 123
115	Literal
116	ExprTuple	124, 125
117	Operation	operator: 151 operand: 134
118	Operation	operator: 147 operands: 127
119	Literal
120	Operation	operator: 128 operands: 129
121	Operation	operator: 130 operands: 131
122	Literal
123	Variable
124	Operation	operator: 147 operands: 132
125	Operation	operator: 147 operands: 133
126	ExprTuple	134
127	ExprTuple	135, 153
128	Literal
129	ExprTuple	136, 149
130	Literal
131	ExprTuple	137, 149
132	ExprTuple	149, 153
133	ExprTuple	149, 138
134	Operation	operator: 139 operands: 140
135	Variable
136	Literal
137	Operation	operator: 141 operands: 142
138	Literal
139	Literal
140	ExprTuple	143, 144
141	Literal
142	ExprTuple	145, 146
143	Literal
144	Operation	operator: 147 operands: 148
145	Literal
146	Variable
147	Literal
148	ExprTuple	149, 150
149	Literal
150	Operation	operator: 151 operand: 153
151	Literal
152	ExprTuple	153
153	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 ¶