Expression of type Conditional ¶

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 Conditional, ExprRange, U, Variable, VertExprArray, eps, m, n, s, t
from proveit.logic import And, InSet
from proveit.numbers import Add, Ceil, Exp, Interval, LessEq, Log, ModAbs, Mult, NaturalPos, Neg, frac, greater_eq, one, subtract, two, zero
from proveit.physics.quantum import I, NumKet, Z, ket_plus, var_ket_u
from proveit.physics.quantum.QPE import QPE, phase, 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 = Conditional(greater_eq(ProbOfAll(instance_param_or_params = [m], instance_element = Qcircuit(vert_expr_array = VertExprArray([ExprRange(sub_expr1, Input(state = ket_plus), one, t), ExprRange(sub_expr1, MultiQubitElem(element = Input(state = var_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), ExprRange(sub_expr1, Gate(operation = I).with_implicit_representation(), one, s)], [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(m, t), part = sub_expr1), targets = Interval(one, t)), one, t), ExprRange(sub_expr1, MultiQubitElem(element = Output(state = var_ket_u, part = sub_expr1), targets = sub_expr4), one, s)])), domain = Interval(zero, subtract(two_pow_t, one)), condition = LessEq(ModAbs(subtract(frac(m, two_pow_t), phase), one), Exp(two, Neg(n)))).with_wrapping(), subtract(one, eps)), And(InSet(t, NaturalPos), greater_eq(t, Add(n, Ceil(Log(two, Add(two, frac(one, Mult(two, eps)))))))))

# 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\{\left[\begin{array}{l}\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)\end{array}\right] \geq \left(1 - \epsilon\right) \textrm{ if } t \in \mathbb{N}^+ ,  t \geq \left(n + \left\lceil \textrm{log}_2\left(2 + \frac{1}{2 \cdot \epsilon}\right)\right\rceil\right)\right..

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

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

Expression of type Conditional¶

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

Expression of type Conditional ¶

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