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, Mult, 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))
expr = Lambda(phase, 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:

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

\varphi \mapsto \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()

no style options

# display the expression information
stored_expr.expr_info()

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