Expression of type ExprTuple

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, ExprTuple, Lambda, Literal, Variable, VertExprArray, e, m
from proveit.logic import And, InSet
from proveit.numbers import Add, Exp, Interval, LessEq, ModAbs, 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 = ExprTuple(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))), LessEq(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())

\left(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}} \leq e\right..\right)

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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