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, 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)), InSet(phase, IntervalCO(zero, one)))))

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