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