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, 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, _full_domain, _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))
sub_expr6 = greater(ModAbs(l, _two_pow_t), e)
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_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)]))
expr = ExprTuple(Conditional(sub_expr7, And(InSet(l, Union(_neg_domain, _pos_domain)), sub_expr6)), Conditional(sub_expr7, And(InSet(l, _full_domain), sub_expr6)))

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