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, l, m
from proveit.logic import And, Bijections, InSet
from proveit.numbers import Add, Interval, Mod, one
from proveit.physics.quantum import NumKet, Z, ket_plus
from proveit.physics.quantum.QPE import ModAdd, QPE, _Omega, _U, _b_floor, _full_domain, _ket_u, _m_domain, _phase_est_circuit, _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(And(InSet(Lambda(l, Mod(Add(_b_floor, l), _two_pow_t)), Bijections(_full_domain, _m_domain)), InSet(Lambda(m, _phase_est_circuit), Bijections(_m_domain, _Omega))), InSet(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))), Bijections(_full_domain, _Omega)))

# 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(\left(\left[l \mapsto \left(\left(b_{\textit{f}} + l\right) ~\textup{mod}~ 2^{t}\right)\right] \in \left[\{-2^{t - 1} + 1~\ldotp \ldotp~2^{t - 1}\} \xrightarrow[\text{onto}]{\text{1-to-1}} \{0~\ldotp \ldotp~2^{t} - 1\}\right]\right) \land \left(\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}\right)\right] \in \left[\{0~\ldotp \ldotp~2^{t} - 1\} \xrightarrow[\text{onto}]{\text{1-to-1}} \Omega\right]\right), \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 \{-2^{t - 1} + 1~\ldotp \ldotp~2^{t - 1}\}\right..\right] \in \left[\{-2^{t - 1} + 1~\ldotp \ldotp~2^{t - 1}\} \xrightarrow[\text{onto}]{\text{1-to-1}} \Omega\right]\right)

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

name	description	default	current value	related methods
wrap_positions	position(s) at which wrapping is to occur; 'n' is after the nth comma.	()	()	('with_wrapping_at',)
justification	if any wrap positions are set, justify to the 'left', 'center', or 'right'	left	left	('with_justification',)

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

Expression of type ExprTuple¶

from the theory of proveit.physics.quantum.QPE¶

Expression of type ExprTuple ¶

from the theory of proveit.physics.quantum.QPE ¶