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