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, 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))
sub_expr7 = 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))))
expr = Equals(Conditional(sub_expr7, InSet(t, NaturalPos)), sub_expr7)

# 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)\right.. \textrm{ if } t \in \mathbb{N}^+\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..

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