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

expr:

# 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[\left(s, t, U, \lvert u \rangle, \varphi\right) \mapsto \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) ,  \varphi \in \left[0,1\right)\right.. \textrm{ if } t \in \mathbb{N}^+\right..\right] =  \\ \left[\left(s, t, U, \lvert u \rangle, \varphi\right) \mapsto \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..\right] \end{array} \end{array}

stored_expr.style_options()

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.	()	(2)	('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')

# display the expression information
stored_expr.expr_info()

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