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 Add, Interval, ModAbs, greater, one
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, _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 = 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)]))
expr = Equals(ProbOfAll(instance_param_or_params = sub_expr2, instance_element = sub_expr7, domain = Union(_neg_domain, _pos_domain), condition = greater(ModAbs(l, _two_pow_t), e)), Add(ProbOfAll(instance_param_or_params = sub_expr2, instance_element = sub_expr7, domain = _neg_domain), ProbOfAll(instance_param_or_params = sub_expr2, instance_element = sub_expr7, domain = _pos_domain)))

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