Expression of type QcircuitEquiv ¶

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, ConditionalSet, ExprRange, Variable, VertExprArray, t
from proveit.linear_algebra import MatrixExp, ScalarMult, VecAdd
from proveit.logic import Equals, NotEquals, Set
from proveit.numbers import Add, Exp, Interval, Mult, Neg, e, frac, i, one, pi, sqrt, two, zero
from proveit.physics.quantum import CONTROL, ket0, ket1, ket_plus
from proveit.physics.quantum.QPE import QPE1, _U, _ket_u, _phase, _s
from proveit.physics.quantum.circuits import Gate, Igate, Input, MultiQubitElem, Output, Qcircuit, QcircuitEquiv

# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = Variable("_b", latex_format = r"{_{-}b}")
sub_expr3 = Add(t, one)
sub_expr4 = Add(t, _s)
sub_expr5 = Add(sub_expr2, t)
sub_expr6 = Interval(sub_expr3, sub_expr4)
sub_expr7 = Add(Neg(t), one)
sub_expr8 = MultiQubitElem(element = Gate(operation = QPE1(_U, t), part = sub_expr1), targets = Interval(one, sub_expr4))
sub_expr9 = [ExprRange(sub_expr1, Input(state = ket_plus), one, t), ExprRange(sub_expr1, MultiQubitElem(element = Input(state = _ket_u, part = sub_expr1), targets = sub_expr6), one, _s)]
sub_expr10 = [ExprRange(sub_expr1, Output(state = ScalarMult(frac(one, sqrt(two)), VecAdd(ket0, ScalarMult(Exp(e, Mult(two, pi, i, Exp(two, Neg(sub_expr1)), _phase)), ket1)))), sub_expr7, zero).with_decreasing_order(), ExprRange(sub_expr1, MultiQubitElem(element = Output(state = _ket_u, part = sub_expr1), targets = sub_expr6), one, _s)]
expr = QcircuitEquiv(Qcircuit(vert_expr_array = VertExprArray(sub_expr9, ExprRange(sub_expr2, [ExprRange(sub_expr1, ConditionalSet(Conditional(MultiQubitElem(element = CONTROL, targets = Set(sub_expr3)), Equals(sub_expr5, sub_expr1)), Conditional(Igate, NotEquals(sub_expr5, sub_expr1))), one, t).with_case_simplification(), ExprRange(sub_expr1, MultiQubitElem(element = Gate(operation = MatrixExp(_U, Exp(two, Neg(sub_expr2))), part = sub_expr1), targets = sub_expr6), one, _s)], sub_expr7, zero).with_decreasing_order(), sub_expr10)), Qcircuit(vert_expr_array = VertExprArray(sub_expr9, [ExprRange(sub_expr1, sub_expr8, one, t), ExprRange(sub_expr1, sub_expr8, sub_expr3, sub_expr4)], sub_expr10))).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(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \control{} \qw \qwx[1] & \qw & \gate{\cdots} \qwx[1] & \qw & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot 2^{t - 1} \cdot \varphi} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\lvert + \rangle} & \qw \qwx[1] & \control{} \qw \qwx[1] & \gate{\cdots} \qwx[1] & \qw & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot 2^{t - 2} \cdot \varphi} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} & \gate{\vdots} \qwx[1] & \gate{\vdots} \qwx[1] & \gate{\ddots} \qwx[1] & \gate{\vdots} & \qout{\vdots} \\
\qin{\lvert + \rangle} & \qw \qwx[1] & \qw \qwx[1] & \gate{\cdots} \qwx[1] & \control{} \qw \qwx[1] & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot 2^{0} \cdot \varphi} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\lvert u \rangle} & \gate{U^{2^{t - 1}}} & \gate{U^{2^{t - 2}}} & \gate{\cdots} & \gate{U^{2^{0}}} & \qout{\lvert u \rangle}
} \end{array}\right) \\  \cong \left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \multigate{4}{\textrm{QPE}_1\left(U, t\right)} & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot 2^{t - 1} \cdot \varphi} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}_1\left(U, t\right)} & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot 2^{t - 2} \cdot \varphi} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} & \ghost{\textrm{QPE}_1\left(U, t\right)} & \qout{\vdots} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}_1\left(U, t\right)} & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot 2^{0} \cdot \varphi} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}_1\left(U, t\right)} & \qout{\lvert u \rangle}
} \end{array}\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: 1 operands: 2
1	Literal
2	ExprTuple	3, 4
3	Operation	operator: 6 operands: 5
4	Operation	operator: 6 operands: 7
5	ExprTuple	9, 8, 11
6	Literal
7	ExprTuple	9, 10, 11
8	ExprRange	lambda_map: 12 start_index: 24 end_index: 112
9	ExprTuple	13, 14
10	ExprTuple	15, 16
11	ExprTuple	17, 18
12	Lambda	parameter: 132 body: 19
13	ExprRange	lambda_map: 20 start_index: 128 end_index: 127
14	ExprRange	lambda_map: 21 start_index: 128 end_index: 110
15	ExprRange	lambda_map: 22 start_index: 128 end_index: 127
16	ExprRange	lambda_map: 22 start_index: 115 end_index: 90
17	ExprRange	lambda_map: 23 start_index: 24 end_index: 112
18	ExprRange	lambda_map: 25 start_index: 128 end_index: 110
19	ExprTuple	26, 27
20	Lambda	parameter: 143 body: 28
21	Lambda	parameter: 143 body: 29
22	Lambda	parameter: 143 body: 30
23	Lambda	parameter: 143 body: 31
24	Operation	operator: 122 operands: 32
25	Lambda	parameter: 143 body: 33
26	ExprRange	lambda_map: 34 start_index: 128 end_index: 127
27	ExprRange	lambda_map: 35 start_index: 128 end_index: 110
28	Operation	operator: 55 operands: 36
29	Operation	operator: 82 operands: 37
30	Operation	operator: 82 operands: 38
31	Operation	operator: 59 operands: 39
32	ExprTuple	40, 128
33	Operation	operator: 82 operands: 41
34	Lambda	parameter: 143 body: 42
35	Lambda	parameter: 143 body: 43
36	NamedExprs	state: 44
37	NamedExprs	element: 45 targets: 64
38	NamedExprs	element: 46 targets: 47
39	NamedExprs	state: 48
40	Operation	operator: 141 operand: 127
41	NamedExprs	element: 50 targets: 64
42	Operation	operator: 51 operands: 52
43	Operation	operator: 82 operands: 53
44	Operation	operator: 120 operand: 65
45	Operation	operator: 55 operands: 60
46	Operation	operator: 85 operands: 56
47	Operation	operator: 75 operands: 57
48	Operation	operator: 103 operands: 58
49	ExprTuple	127
50	Operation	operator: 59 operands: 60
51	Literal
52	ExprTuple	61, 62
53	NamedExprs	element: 63 targets: 64
54	ExprTuple	65
55	Literal
56	NamedExprs	operation: 66 part: 143
57	ExprTuple	128, 90
58	ExprTuple	67, 68
59	Literal
60	NamedExprs	state: 69 part: 143
61	Conditional	value: 70 condition: 71
62	Conditional	value: 72 condition: 73
63	Operation	operator: 85 operands: 74
64	Operation	operator: 75 operands: 76
65	Literal
66	Operation	operator: 77 operands: 78
67	Operation	operator: 117 operands: 79
68	Operation	operator: 80 operands: 81
69	Literal
70	Operation	operator: 82 operands: 83
71	Operation	operator: 84 operands: 88
72	Operation	operator: 85 operands: 86
73	Operation	operator: 87 operands: 88
74	NamedExprs	operation: 89 part: 143
75	Literal
76	ExprTuple	115, 90
77	Literal
78	ExprTuple	108, 127
79	ExprTuple	128, 91
80	Literal
81	ExprTuple	92, 93
82	Literal
83	NamedExprs	element: 94 targets: 95
84	Literal
85	Literal
86	NamedExprs	operation: 96
87	Literal
88	ExprTuple	97, 143
89	Operation	operator: 98 operands: 99
90	Operation	operator: 122 operands: 100
91	Operation	operator: 137 operands: 101
92	Operation	operator: 120 operand: 112
93	Operation	operator: 103 operands: 104
94	Literal
95	Operation	operator: 105 operand: 115
96	Literal
97	Operation	operator: 122 operands: 107
98	Literal
99	ExprTuple	108, 109
100	ExprTuple	127, 110
101	ExprTuple	139, 111
102	ExprTuple	112
103	Literal
104	ExprTuple	113, 114
105	Literal
106	ExprTuple	115
107	ExprTuple	132, 127
108	Literal
109	Operation	operator: 137 operands: 116
110	Literal
111	Operation	operator: 117 operands: 118
112	Literal
113	Operation	operator: 137 operands: 119
114	Operation	operator: 120 operand: 128
115	Operation	operator: 122 operands: 123
116	ExprTuple	139, 124
117	Literal
118	ExprTuple	128, 139
119	ExprTuple	125, 126
120	Literal
121	ExprTuple	128
122	Literal
123	ExprTuple	127, 128
124	Operation	operator: 141 operand: 132
125	Literal
126	Operation	operator: 130 operands: 131
127	Variable
128	Literal
129	ExprTuple	132
130	Literal
131	ExprTuple	139, 133, 134, 135, 136
132	Variable
133	Literal
134	Literal
135	Operation	operator: 137 operands: 138
136	Literal
137	Literal
138	ExprTuple	139, 140
139	Literal
140	Operation	operator: 141 operand: 143
141	Literal
142	ExprTuple	143
143	Variable

Expression of type QcircuitEquiv¶

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

Expression of type QcircuitEquiv ¶

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