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
from proveit.logic import And, Equals, Forall, InSet
from proveit.numbers import Add, Exp, Interval, IntervalCO, Mod, Mult, 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_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 = [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(), And(InSet(var_ket_u, s_ket_domain), normalized_var_ket_u))

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