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 ExprRange, ExprTuple, Variable, VertExprArray, e, l
from proveit.logic import 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
from proveit.statistics import ProbOfAll

# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = [l]
sub_expr3 = Add(_t, one)
sub_expr4 = Add(_t, _s)
sub_expr5 = Interval(sub_expr3, sub_expr4)
sub_expr6 = MultiQubitElem(element = Gate(operation = QPE(_U, _t), part = sub_expr1), targets = Interval(one, sub_expr4))
sub_expr7 = 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_expr5), one, _s)], [ExprRange(sub_expr1, sub_expr6, one, _t), ExprRange(sub_expr1, sub_expr6, sub_expr3, sub_expr4)], [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_expr5), one, _s)]))
expr = ExprTuple(ProbOfAll(instance_param_or_params = sub_expr2, instance_element = sub_expr7, domain = Union(_neg_domain, _pos_domain), condition = greater(ModAbs(l, _two_pow_t), e)), Add(ProbOfAll(instance_param_or_params = sub_expr2, instance_element = sub_expr7, domain = _neg_domain), ProbOfAll(instance_param_or_params = sub_expr2, instance_element = sub_expr7, domain = _pos_domain)))

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