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, 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 _U, _ket_u, _phase, _s
from proveit.physics.quantum.circuits import Gate, Igate, Input, 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 = Variable("_b", latex_format = r"{_{-}b}")
sub_expr3 = Add(t, one)
sub_expr4 = Add(sub_expr2, t)
sub_expr5 = Interval(sub_expr3, Add(t, _s))
sub_expr6 = Add(Neg(t), one)
expr = Equals(Prob(Qcircuit(vert_expr_array = VertExprArray([ExprRange(sub_expr1, Input(state = ket_plus), one, t), ExprRange(sub_expr1, MultiQubitElem(element = Input(state = _ket_u, part = sub_expr1), targets = sub_expr5), one, _s)], ExprRange(sub_expr2, [ExprRange(sub_expr1, ConditionalSet(Conditional(MultiQubitElem(element = CONTROL, targets = Set(sub_expr3)), Equals(sub_expr4, sub_expr1)), Conditional(Igate, NotEquals(sub_expr4, 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_expr5), one, _s)], sub_expr6, zero).with_decreasing_order(), [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_expr6, zero).with_decreasing_order(), ExprRange(sub_expr1, MultiQubitElem(element = Output(state = _ket_u, part = sub_expr1), targets = sub_expr5), one, _s)]))), 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())

\textrm{Pr}\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) = 1

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