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, Variable, VertExprArray, e, l
from proveit.logic import And, InSet, Union
from proveit.numbers import Add, Interval, ModAbs, greater, 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, _pos_domain, _s, _s_wire, _t, _two_pow_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 = ExprTuple(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)])), And(InSet(l, Union(_neg_domain, _pos_domain)), greater(ModAbs(l, _two_pow_t), 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(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 \left(\{-2^{t - 1} + 1~\ldotp \ldotp~-\left(e + 1\right)\} \cup \{e + 1~\ldotp \ldotp~2^{t - 1}\}\right) ,  \left|l\right|_{\textup{mod}\thinspace 2^{t}} > 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: 115 body: 3
2	ExprTuple	115
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: 126 end_index: 122
17	ExprRange	lambda_map: 29 start_index: 126 end_index: 107
18	ExprRange	lambda_map: 30 start_index: 126 end_index: 122
19	ExprRange	lambda_map: 30 start_index: 93 end_index: 94
20	ExprRange	lambda_map: 31 start_index: 126 end_index: 122
21	ExprRange	lambda_map: 32 start_index: 126 end_index: 107
22	ExprRange	lambda_map: 33 start_index: 126 end_index: 122
23	ExprRange	lambda_map: 34 start_index: 126 end_index: 107
24	Literal
25	ExprTuple	115, 35
26	Literal
27	ExprTuple	113, 36
28	Lambda	parameter: 92 body: 37
29	Lambda	parameter: 92 body: 38
30	Lambda	parameter: 92 body: 39
31	Lambda	parameter: 92 body: 40
32	Lambda	parameter: 92 body: 41
33	Lambda	parameter: 92 body: 42
34	Lambda	parameter: 92 body: 44
35	Operation	operator: 45 operands: 46
36	Operation	operator: 47 operands: 48
37	Operation	operator: 76 operands: 49
38	Operation	operator: 56 operands: 50
39	Operation	operator: 56 operands: 51
40	Operation	operator: 52 operands: 53
41	Operation	operator: 77 operands: 54
42	Operation	operator: 56 operands: 55
43	ExprTuple	92
44	Operation	operator: 56 operands: 57
45	Literal
46	ExprTuple	58, 59
47	Literal
48	ExprTuple	115, 60
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	Operation	operator: 84 operands: 71
59	Operation	operator: 84 operands: 72
60	Operation	operator: 116 operands: 73
61	Operation	operator: 74 operand: 88
62	Operation	operator: 76 operands: 83
63	Operation	operator: 77 operands: 78
64	Operation	operator: 84 operands: 79
65	Literal
66	Literal
67	Operation	operator: 82 operands: 80
68	Operation	operator: 84 operands: 81
69	Operation	operator: 82 operands: 83
70	Operation	operator: 84 operands: 85
71	ExprTuple	86, 87
72	ExprTuple	104, 112
73	ExprTuple	118, 122
74	Literal
75	ExprTuple	88
76	Literal
77	Literal
78	NamedExprs	operation: 89 part: 92
79	ExprTuple	126, 94
80	NamedExprs	state: 90 part: 92
81	ExprTuple	126, 122
82	Literal
83	NamedExprs	state: 91 part: 92
84	Literal
85	ExprTuple	93, 94
86	Operation	operator: 120 operands: 95
87	Operation	operator: 124 operand: 104
88	Literal
89	Operation	operator: 97 operands: 98
90	Operation	operator: 99 operands: 100
91	Literal
92	Variable
93	Operation	operator: 120 operands: 101
94	Operation	operator: 120 operands: 102
95	ExprTuple	103, 126
96	ExprTuple	104
97	Literal
98	ExprTuple	105, 122
99	Literal
100	ExprTuple	106, 122
101	ExprTuple	122, 126
102	ExprTuple	122, 107
103	Operation	operator: 124 operand: 112
104	Operation	operator: 120 operands: 109
105	Literal
106	Operation	operator: 110 operands: 111
107	Literal
108	ExprTuple	112
109	ExprTuple	113, 126
110	Literal
111	ExprTuple	114, 115
112	Operation	operator: 116 operands: 117
113	Variable
114	Literal
115	Variable
116	Literal
117	ExprTuple	118, 119
118	Literal
119	Operation	operator: 120 operands: 121
120	Literal
121	ExprTuple	122, 123
122	Literal
123	Operation	operator: 124 operand: 126
124	Literal
125	ExprTuple	126
126	Literal