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, s, t
from proveit.linear_algebra import MatrixMult, ScalarMult, Unitary
from proveit.logic import And, Equals, Forall, InSet
from proveit.numbers import Add, Exp, Interval, IntervalCO, Mod, Mult, NaturalPos, Real, Round, e, four, frac, greater, i, one, pi, two, zero
from proveit.physics.quantum import I, NumKet, Z, ket_plus, normalized_var_ket_u, var_ket_u
from proveit.physics.quantum.QPE import QPE, phase, s_ket_domain, two_pow_s, two_pow_t
from proveit.physics.quantum.circuits import Gate, Input, Measure, MultiQubitElem, Output, Qcircuit
from proveit.statistics import Prob

# 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(Forall(instance_param_or_params = [U], instance_expr = Forall(instance_param_or_params = [var_ket_u], instance_expr = Forall(instance_param_or_params = [phase], instance_expr = greater(Prob(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(Mod(Round(Mult(two_pow_t, phase)), two_pow_t), 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)]))), frac(four, Exp(pi, two))), domain = Real, conditions = [InSet(phase, IntervalCO(zero, one)), Equals(MatrixMult(U, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, phase)), var_ket_u))]).with_wrapping(), domain = s_ket_domain, condition = normalized_var_ket_u).with_wrapping(), domain = Unitary(two_pow_s)).with_wrapping(), And(InSet(s, NaturalPos), InSet(t, NaturalPos)))

# 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\{\begin{array}{l}\forall_{U \in \textrm{U}\left(2^{s}\right)}~\\
\left[\begin{array}{l}\forall_{\lvert u \rangle \in \mathbb{C}^{2^{s}}~|~\left \|\lvert u \rangle\right \| = 1}~\\
\left[\begin{array}{l}\forall_{\varphi \in \mathbb{R}~|~\varphi \in \left[0,1\right), \left(U \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi} \cdot \lvert u \rangle\right)}~\\
\left(\textrm{Pr}\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \multigate{4}{\textrm{QPE}\left(U, t\right)} & \meter & \multiqout{3}{\lvert round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \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 round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right) > \frac{4}{\pi^{2}}\right)\end{array}\right]\end{array}\right]\end{array} \textrm{ if } s \in \mathbb{N}^+ ,  t \in \mathbb{N}^+\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: 24 operand: 5
2	Operation	operator: 40 operands: 4
3	ExprTuple	5
4	ExprTuple	6, 7
5	Lambda	parameter: 159 body: 9
6	Operation	operator: 58 operands: 10
7	Operation	operator: 58 operands: 11
8	ExprTuple	159
9	Conditional	value: 12 condition: 13
10	ExprTuple	162, 14
11	ExprTuple	176, 14
12	Operation	operator: 24 operand: 17
13	Operation	operator: 58 operands: 16
14	Literal
15	ExprTuple	17
16	ExprTuple	159, 18
17	Lambda	parameter: 148 body: 19
18	Operation	operator: 20 operand: 52
19	Conditional	value: 22 condition: 23
20	Literal
21	ExprTuple	52
22	Operation	operator: 24 operand: 27
23	Operation	operator: 40 operands: 26
24	Literal
25	ExprTuple	27
26	ExprTuple	28, 29
27	Lambda	parameter: 172 body: 31
28	Operation	operator: 58 operands: 32
29	Operation	operator: 60 operands: 33
30	ExprTuple	172
31	Conditional	value: 34 condition: 35
32	ExprTuple	148, 36
33	ExprTuple	37, 161
34	Operation	operator: 38 operands: 39
35	Operation	operator: 40 operands: 41
36	Operation	operator: 42 operands: 43
37	Operation	operator: 44 operand: 148
38	Literal
39	ExprTuple	46, 47
40	Literal
41	ExprTuple	48, 49, 50
42	Literal
43	ExprTuple	51, 52
44	Literal
45	ExprTuple	148
46	Operation	operator: 53 operands: 54
47	Operation	operator: 55 operand: 65
48	Operation	operator: 58 operands: 57
49	Operation	operator: 58 operands: 59
50	Operation	operator: 60 operands: 61
51	Literal
52	Operation	operator: 173 operands: 62
53	Literal
54	ExprTuple	63, 64
55	Literal
56	ExprTuple	65
57	ExprTuple	172, 66
58	Literal
59	ExprTuple	172, 67
60	Literal
61	ExprTuple	68, 69
62	ExprTuple	175, 162
63	Literal
64	Operation	operator: 173 operands: 70
65	Operation	operator: 71 operands: 72
66	Literal
67	Operation	operator: 73 operands: 74
68	Operation	operator: 75 operands: 76
69	Operation	operator: 77 operands: 78
70	ExprTuple	121, 175
71	Literal
72	ExprTuple	79, 80, 81, 82
73	Literal
74	ExprTuple	83, 161
75	Literal
76	ExprTuple	159, 148
77	Literal
78	ExprTuple	84, 148
79	ExprTuple	85, 86
80	ExprTuple	87, 88
81	ExprTuple	89, 90
82	ExprTuple	91, 92
83	Literal
84	Operation	operator: 173 operands: 93
85	ExprRange	lambda_map: 94 start_index: 161 end_index: 176
86	ExprRange	lambda_map: 95 start_index: 161 end_index: 162
87	ExprRange	lambda_map: 96 start_index: 161 end_index: 176
88	ExprRange	lambda_map: 96 start_index: 150 end_index: 151
89	ExprRange	lambda_map: 97 start_index: 161 end_index: 176
90	ExprRange	lambda_map: 98 start_index: 161 end_index: 162
91	ExprRange	lambda_map: 99 start_index: 161 end_index: 176
92	ExprRange	lambda_map: 100 start_index: 161 end_index: 162
93	ExprTuple	101, 102
94	Lambda	parameter: 149 body: 103
95	Lambda	parameter: 149 body: 104
96	Lambda	parameter: 149 body: 105
97	Lambda	parameter: 149 body: 106
98	Lambda	parameter: 149 body: 107
99	Lambda	parameter: 149 body: 108
100	Lambda	parameter: 149 body: 110
101	Literal
102	Operation	operator: 169 operands: 111
103	Operation	operator: 135 operands: 112
104	Operation	operator: 119 operands: 113
105	Operation	operator: 119 operands: 114
106	Operation	operator: 115 operands: 116
107	Operation	operator: 136 operands: 117
108	Operation	operator: 119 operands: 118
109	ExprTuple	149
110	Operation	operator: 119 operands: 120
111	ExprTuple	175, 121, 122, 172
112	NamedExprs	state: 123
113	NamedExprs	element: 124 targets: 132
114	NamedExprs	element: 125 targets: 126
115	Literal
116	NamedExprs	basis: 127
117	NamedExprs	operation: 128
118	NamedExprs	element: 129 targets: 130
119	Literal
120	NamedExprs	element: 131 targets: 132
121	Literal
122	Literal
123	Operation	operator: 133 operand: 145
124	Operation	operator: 135 operands: 142
125	Operation	operator: 136 operands: 137
126	Operation	operator: 143 operands: 138
127	Literal
128	Literal
129	Operation	operator: 141 operands: 139
130	Operation	operator: 143 operands: 140
131	Operation	operator: 141 operands: 142
132	Operation	operator: 143 operands: 144
133	Literal
134	ExprTuple	145
135	Literal
136	Literal
137	NamedExprs	operation: 146 part: 149
138	ExprTuple	161, 151
139	NamedExprs	state: 147 part: 149
140	ExprTuple	161, 176
141	Literal
142	NamedExprs	state: 148 part: 149
143	Literal
144	ExprTuple	150, 151
145	Literal
146	Operation	operator: 152 operands: 153
147	Operation	operator: 154 operands: 155
148	Variable
149	Variable
150	Operation	operator: 157 operands: 156
151	Operation	operator: 157 operands: 158
152	Literal
153	ExprTuple	159, 176
154	Literal
155	ExprTuple	160, 176
156	ExprTuple	176, 161
157	Literal
158	ExprTuple	176, 162
159	Variable
160	Operation	operator: 163 operands: 164
161	Literal
162	Variable
163	Literal
164	ExprTuple	165, 171
165	Operation	operator: 166 operand: 168
166	Literal
167	ExprTuple	168
168	Operation	operator: 169 operands: 170
169	Literal
170	ExprTuple	171, 172
171	Operation	operator: 173 operands: 174
172	Variable
173	Literal
174	ExprTuple	175, 176
175	Literal
176	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 ¶