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, Literal, Variable, VertExprArray, e, m
from proveit.logic import And, InSet
from proveit.numbers import Add, Exp, Interval, ModAbs, greater, one, subtract, two, zero
from proveit.physics.quantum import I, NumKet, Z, ket_plus
from proveit.physics.quantum.QPE import QPE
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(Literal("t", theory = "proveit.physics.quantum.QPE"), one)
sub_expr3 = Add(Literal("t", theory = "proveit.physics.quantum.QPE"), Literal("s", theory = "proveit.physics.quantum.QPE"))
sub_expr4 = Exp(two, Literal("t", theory = "proveit.physics.quantum.QPE"))
sub_expr5 = Interval(sub_expr2, sub_expr3)
sub_expr6 = MultiQubitElem(element = Gate(operation = QPE(Literal("U", theory = "proveit.physics.quantum.QPE"), Literal("t", theory = "proveit.physics.quantum.QPE")), part = sub_expr1), targets = Interval(one, sub_expr3))
expr = Lambda(m, Conditional(Qcircuit(vert_expr_array = VertExprArray([ExprRange(sub_expr1, Input(state = ket_plus), one, Literal("t", theory = "proveit.physics.quantum.QPE")), ExprRange(sub_expr1, MultiQubitElem(element = Input(state = Literal("|u>", latex_format = r"\lvert u \rangle", theory = "proveit.physics.quantum.QPE"), part = sub_expr1), targets = sub_expr5), one, Literal("s", theory = "proveit.physics.quantum.QPE"))], [ExprRange(sub_expr1, sub_expr6, one, Literal("t", theory = "proveit.physics.quantum.QPE")), ExprRange(sub_expr1, sub_expr6, sub_expr2, sub_expr3)], [ExprRange(sub_expr1, Measure(basis = Z), one, Literal("t", theory = "proveit.physics.quantum.QPE")), ExprRange(sub_expr1, Gate(operation = I).with_implicit_representation(), one, Literal("s", theory = "proveit.physics.quantum.QPE"))], [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(m, Literal("t", theory = "proveit.physics.quantum.QPE")), part = sub_expr1), targets = Interval(one, Literal("t", theory = "proveit.physics.quantum.QPE"))), one, Literal("t", theory = "proveit.physics.quantum.QPE")), ExprRange(sub_expr1, MultiQubitElem(element = Output(state = Literal("|u>", latex_format = r"\lvert u \rangle", theory = "proveit.physics.quantum.QPE"), part = sub_expr1), targets = sub_expr5), one, Literal("s", theory = "proveit.physics.quantum.QPE"))])), And(InSet(m, Interval(zero, subtract(sub_expr4, one))), greater(ModAbs(subtract(m, Literal("b_{f}", latex_format = r"b_{\textit{f}}", theory = "proveit.physics.quantum.QPE")), sub_expr4), e))))

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

m \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 m \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert m \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 m \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert m \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array} \textrm{ if } m \in \{0~\ldotp \ldotp~2^{t} - 1\} ,  \left|m - b_{\textit{f}}\right|_{\textup{mod}\thinspace 2^{t}} > e\right..

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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