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, 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(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))))

# 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\{\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..

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