Expression of type NamedExprs

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, Function, Lambda, NamedExprs, Variable, VertExprArray, e, l
from proveit.logic import And, Equals, InSet, Union
from proveit.numbers import Abs, Add, Exp, Interval, ModAbs, Sum, greater, one, two
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, _rel_indexed_alpha, _s, _s_wire, _t, _two_pow_t
from proveit.physics.quantum.circuits import Gate, Input, Measure, MultiQubitElem, Output, Qcircuit
from proveit.statistics import ProbOfAll

# build up the expression from sub-expressions
sub_expr1 = Variable("_b", latex_format = r"{_{-}b}")
sub_expr2 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr3 = [l]
sub_expr4 = Add(_t, one)
sub_expr5 = Add(_t, _s)
sub_expr6 = Interval(sub_expr4, sub_expr5)
sub_expr7 = MultiQubitElem(element = Gate(operation = QPE(_U, _t), part = sub_expr2), targets = Interval(one, sub_expr5))
sub_expr8 = Exp(Abs(_rel_indexed_alpha), two)
expr = NamedExprs(("lambda", Lambda(sub_expr1, Equals(ProbOfAll(instance_param_or_params = sub_expr3, instance_element = Function(sub_expr1, sub_expr3)), Add(Sum(index_or_indices = sub_expr3, summand = sub_expr8, domain = _neg_domain), Sum(index_or_indices = sub_expr3, summand = sub_expr8, domain = _pos_domain))).with_wrapping_at(2))), ("${_{-}b}$", Conditional(Qcircuit(vert_expr_array = VertExprArray([ExprRange(sub_expr2, Input(state = ket_plus), one, _t), ExprRange(sub_expr2, MultiQubitElem(element = Input(state = _ket_u, part = sub_expr2), targets = sub_expr6), one, _s)], [ExprRange(sub_expr2, sub_expr7, one, _t), ExprRange(sub_expr2, sub_expr7, sub_expr4, sub_expr5)], [ExprRange(sub_expr2, Measure(basis = Z), one, _t), _s_wire], [ExprRange(sub_expr2, MultiQubitElem(element = Output(state = NumKet(ModAdd(_b_floor, l), _t), part = sub_expr2), targets = Interval(one, _t)), one, _t), ExprRange(sub_expr2, MultiQubitElem(element = Output(state = _ket_u, part = sub_expr2), targets = sub_expr6), 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\{ \begin{array}{l}
{\rm lambda}: \left[{_{-}b} \mapsto \left(\begin{array}{c} \begin{array}{l} \left[\textrm{Prob}_{l}~{_{-}b}\left(l\right)\right] =  \\ \left(\left(\sum_{l = -2^{t - 1} + 1}^{-\left(e + 1\right)} \left|\alpha_{b_{\textit{f}} \oplus l}\right|^{2}\right) + \left(\sum_{l = e + 1}^{2^{t - 1}} \left|\alpha_{b_{\textit{f}} \oplus l}\right|^{2}\right)\right) \end{array} \end{array}\right)\right]\\
{_{-}b}: \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..\\
\end{array} \right\}

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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