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, InSet
from proveit.numbers import Add, Exp, Interval, IntervalCO, Mult, NaturalPos, Real, e, i, one, pi, 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 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(Conditional(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), And(InSet(phase, Real), 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)), InSet(phase, IntervalCO(zero, one)))), 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\{\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 \textrm{ if } \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) ,  \varphi \in \left[0,1\right)\right.. \textrm{ if } 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	Conditional	value: 3 condition: 4
2	Operation	operator: 21 operands: 5
3	Operation	operator: 19 operands: 6
4	Operation	operator: 7 operands: 8
5	ExprTuple	134, 9
6	ExprTuple	10, 125
7	Literal
8	ExprTuple	11, 12, 13, 14
9	Literal
10	Operation	operator: 15 operand: 23
11	Operation	operator: 21 operands: 17
12	Operation	operator: 21 operands: 18
13	Operation	operator: 19 operands: 20
14	Operation	operator: 21 operands: 22
15	Literal
16	ExprTuple	23
17	ExprTuple	130, 24
18	ExprTuple	124, 25
19	Literal
20	ExprTuple	26, 27
21	Literal
22	ExprTuple	130, 28
23	Operation	operator: 29 operands: 30
24	Literal
25	Operation	operator: 107 operands: 31
26	Operation	operator: 32 operands: 33
27	Operation	operator: 34 operands: 35
28	Operation	operator: 36 operands: 37
29	Literal
30	ExprTuple	38, 39, 40, 41
31	ExprTuple	44, 42
32	Literal
33	ExprTuple	123, 112
34	Literal
35	ExprTuple	43, 112
36	Literal
37	ExprTuple	44, 125
38	ExprTuple	45, 46
39	ExprTuple	47, 48
40	ExprTuple	49, 50
41	ExprTuple	51, 52
42	Operation	operator: 121 operands: 53
43	Operation	operator: 131 operands: 54
44	Literal
45	ExprRange	lambda_map: 55 start_index: 125 end_index: 134
46	ExprRange	lambda_map: 56 start_index: 125 end_index: 126
47	ExprRange	lambda_map: 57 start_index: 125 end_index: 134
48	ExprRange	lambda_map: 57 start_index: 114 end_index: 115
49	ExprRange	lambda_map: 58 start_index: 125 end_index: 134
50	ExprRange	lambda_map: 59 start_index: 125 end_index: 126
51	ExprRange	lambda_map: 60 start_index: 125 end_index: 134
52	ExprRange	lambda_map: 61 start_index: 125 end_index: 126
53	ExprTuple	129, 62
54	ExprTuple	63, 64
55	Lambda	parameter: 113 body: 65
56	Lambda	parameter: 113 body: 66
57	Lambda	parameter: 113 body: 67
58	Lambda	parameter: 113 body: 68
59	Lambda	parameter: 113 body: 69
60	Lambda	parameter: 113 body: 70
61	Lambda	parameter: 113 body: 72
62	Operation	operator: 73 operand: 125
63	Literal
64	Operation	operator: 127 operands: 75
65	Operation	operator: 99 operands: 76
66	Operation	operator: 83 operands: 77
67	Operation	operator: 83 operands: 78
68	Operation	operator: 79 operands: 80
69	Operation	operator: 100 operands: 81
70	Operation	operator: 83 operands: 82
71	ExprTuple	113
72	Operation	operator: 83 operands: 84
73	Literal
74	ExprTuple	125
75	ExprTuple	133, 85, 86, 130
76	NamedExprs	state: 87
77	NamedExprs	element: 88 targets: 96
78	NamedExprs	element: 89 targets: 90
79	Literal
80	NamedExprs	basis: 91
81	NamedExprs	operation: 92
82	NamedExprs	element: 93 targets: 94
83	Literal
84	NamedExprs	element: 95 targets: 96
85	Literal
86	Literal
87	Operation	operator: 97 operand: 109
88	Operation	operator: 99 operands: 106
89	Operation	operator: 100 operands: 101
90	Operation	operator: 107 operands: 102
91	Literal
92	Literal
93	Operation	operator: 105 operands: 103
94	Operation	operator: 107 operands: 104
95	Operation	operator: 105 operands: 106
96	Operation	operator: 107 operands: 108
97	Literal
98	ExprTuple	109
99	Literal
100	Literal
101	NamedExprs	operation: 110 part: 113
102	ExprTuple	125, 115
103	NamedExprs	state: 111 part: 113
104	ExprTuple	125, 134
105	Literal
106	NamedExprs	state: 112 part: 113
107	Literal
108	ExprTuple	114, 115
109	Literal
110	Operation	operator: 116 operands: 117
111	Operation	operator: 118 operands: 119
112	Variable
113	Variable
114	Operation	operator: 121 operands: 120
115	Operation	operator: 121 operands: 122
116	Literal
117	ExprTuple	123, 134
118	Literal
119	ExprTuple	124, 134
120	ExprTuple	134, 125
121	Literal
122	ExprTuple	134, 126
123	Variable
124	Operation	operator: 127 operands: 128
125	Literal
126	Variable
127	Literal
128	ExprTuple	129, 130
129	Operation	operator: 131 operands: 132
130	Variable
131	Literal
132	ExprTuple	133, 134
133	Literal
134	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 ¶