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 Equals, Forall, InSet
from proveit.numbers import Add, Exp, Interval, Mult, 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 = [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(), InSet(U, Unitary(two_pow_s)))

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