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, _ket_u, _neg_domain, _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, _neg_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~-\left(e + 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: 106 body: 2
1	ExprTuple	106
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	106, 13
9	ExprTuple	14, 15
10	ExprTuple	16, 17
11	ExprTuple	18, 19
12	ExprTuple	20, 21
13	Operation	operator: 75 operands: 22
14	ExprRange	lambda_map: 23 start_index: 109 end_index: 103
15	ExprRange	lambda_map: 24 start_index: 109 end_index: 98
16	ExprRange	lambda_map: 25 start_index: 109 end_index: 103
17	ExprRange	lambda_map: 25 start_index: 84 end_index: 85
18	ExprRange	lambda_map: 26 start_index: 109 end_index: 103
19	ExprRange	lambda_map: 27 start_index: 109 end_index: 98
20	ExprRange	lambda_map: 28 start_index: 109 end_index: 103
21	ExprRange	lambda_map: 29 start_index: 109 end_index: 98
22	ExprTuple	30, 31
23	Lambda	parameter: 83 body: 32
24	Lambda	parameter: 83 body: 33
25	Lambda	parameter: 83 body: 34
26	Lambda	parameter: 83 body: 35
27	Lambda	parameter: 83 body: 36
28	Lambda	parameter: 83 body: 37
29	Lambda	parameter: 83 body: 39
30	Operation	operator: 99 operands: 40
31	Operation	operator: 107 operand: 52
32	Operation	operator: 67 operands: 42
33	Operation	operator: 49 operands: 43
34	Operation	operator: 49 operands: 44
35	Operation	operator: 45 operands: 46
36	Operation	operator: 68 operands: 47
37	Operation	operator: 49 operands: 48
38	ExprTuple	83
39	Operation	operator: 49 operands: 50
40	ExprTuple	51, 109
41	ExprTuple	52
42	NamedExprs	state: 53
43	NamedExprs	element: 54 targets: 62
44	NamedExprs	element: 55 targets: 56
45	Literal
46	NamedExprs	basis: 57
47	NamedExprs	operation: 58
48	NamedExprs	element: 59 targets: 60
49	Literal
50	NamedExprs	element: 61 targets: 62
51	Operation	operator: 107 operand: 77
52	Operation	operator: 99 operands: 64
53	Operation	operator: 65 operand: 79
54	Operation	operator: 67 operands: 74
55	Operation	operator: 68 operands: 69
56	Operation	operator: 75 operands: 70
57	Literal
58	Literal
59	Operation	operator: 73 operands: 71
60	Operation	operator: 75 operands: 72
61	Operation	operator: 73 operands: 74
62	Operation	operator: 75 operands: 76
63	ExprTuple	77
64	ExprTuple	78, 109
65	Literal
66	ExprTuple	79
67	Literal
68	Literal
69	NamedExprs	operation: 80 part: 83
70	ExprTuple	109, 85
71	NamedExprs	state: 81 part: 83
72	ExprTuple	109, 103
73	Literal
74	NamedExprs	state: 82 part: 83
75	Literal
76	ExprTuple	84, 85
77	Operation	operator: 86 operands: 87
78	Variable
79	Literal
80	Operation	operator: 88 operands: 89
81	Operation	operator: 90 operands: 91
82	Literal
83	Variable
84	Operation	operator: 99 operands: 92
85	Operation	operator: 99 operands: 93
86	Literal
87	ExprTuple	94, 95
88	Literal
89	ExprTuple	96, 103
90	Literal
91	ExprTuple	97, 103
92	ExprTuple	103, 109
93	ExprTuple	103, 98
94	Literal
95	Operation	operator: 99 operands: 100
96	Literal
97	Operation	operator: 101 operands: 102
98	Literal
99	Literal
100	ExprTuple	103, 104
101	Literal
102	ExprTuple	105, 106
103	Literal
104	Operation	operator: 107 operand: 109
105	Literal
106	Variable
107	Literal
108	ExprTuple	109
109	Literal