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, Variable, VertExprArray, l
from proveit.logic import InSet
from proveit.numbers import Add, Interval, one
from proveit.physics.quantum import NumKet, Z, ket_plus
from proveit.physics.quantum.QPE import ModAdd, QPE, _U, _b_floor, _full_domain, _ket_u, _s, _s_wire, _t
from proveit.physics.quantum.circuits import Gate, Input, Measure, MultiQubitElem, Output, Qcircuit

# 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 = MultiQubitElem(element = Gate(operation = QPE(_U, _t), part = sub_expr1), targets = Interval(one, sub_expr3))
expr = Lambda(l, Conditional(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_expr4), one, _s)], [ExprRange(sub_expr1, sub_expr5, one, _t), ExprRange(sub_expr1, sub_expr5, sub_expr2, sub_expr3)], [ExprRange(sub_expr1, Measure(basis = Z), one, _t), _s_wire], [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(ModAdd(_b_floor, l), _t), part = sub_expr1), targets = Interval(one, _t)), one, _t), ExprRange(sub_expr1, MultiQubitElem(element = Output(state = _ket_u, part = sub_expr1), targets = sub_expr4), one, _s)])), InSet(l, _full_domain)))

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

l \mapsto \left\{\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \multigate{4}{\textrm{QPE}\left(U, t\right)} & \meter & \multiqout{3}{\lvert b_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert b_{\textit{f}} \oplus l \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 b_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert b_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array} \textrm{ if } l \in \{-2^{t - 1} + 1~\ldotp \ldotp~2^{t - 1}\}\right..

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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