Expression of type Equals ¶

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 = InSet(phase, Real)
sub_expr5 = Interval(sub_expr2, sub_expr3)
sub_expr6 = Mult(two_pow_t, phase)
sub_expr7 = MultiQubitElem(element = Gate(operation = QPE(U, t), part = sub_expr1), targets = Interval(one, sub_expr3))
sub_expr8 = InSet(sub_expr6, Interval(zero, subtract(two_pow_t, one)))
sub_expr9 = Equals(MatrixMult(U, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, phase)), var_ket_u))
sub_expr10 = 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_expr5), one, s)], [ExprRange(sub_expr1, sub_expr7, one, t), ExprRange(sub_expr1, sub_expr7, 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_expr6, 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_expr5), one, s)]))), one)
expr = Equals(Conditional(sub_expr10, And(sub_expr4, sub_expr8, sub_expr9, InSet(phase, IntervalCO(zero, one)))), Conditional(sub_expr10, And(sub_expr4, sub_expr8, sub_expr9))).with_wrapping_at(1)

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

\begin{array}{c} \begin{array}{l} \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.. \\  = \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)\right.. \end{array} \end{array}

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

name	description	default	current value	related methods
operation	'infix' or 'function' style formatting	infix	infix
wrap_positions	position(s) at which wrapping is to occur; '2 n - 1' is after the nth operand, '2 n' is after the nth operation.	()	(1)	('with_wrapping_at', 'with_wrap_before_operator', 'with_wrap_after_operator', 'without_wrapping', 'wrap_positions')
justification	if any wrap positions are set, justify to the 'left', 'center', or 'right'	center	center	('with_justification',)
direction	Direction of the relation (normal or reversed)	normal	normal	('with_direction_reversed', 'is_reversed')

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

Expression of type Equals¶

from the theory of proveit.physics.quantum.QPE¶

Expression of type Equals ¶

from the theory of proveit.physics.quantum.QPE ¶