Expression of type Lambda

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 = 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 = Lambda([s, t, U, var_ket_u, phase], Conditional(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))), InSet(t, NaturalPos)))

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

\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.. = \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..

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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