Expression of type Conditional ¶

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, Variable, VertExprArray, l
from proveit.logic import InSet
from proveit.numbers import Add, Interval, 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, _s, _s_wire, _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 = 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))

# 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 \{-2^{t - 1} + 1~\ldotp \ldotp~2^{t - 1}\}\right..

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions
0	Conditional	value: 1 condition: 2
1	Operation	operator: 3 operands: 4
2	Operation	operator: 5 operands: 6
3	Literal
4	ExprTuple	7, 8, 9, 10
5	Literal
6	ExprTuple	99, 11
7	ExprTuple	12, 13
8	ExprTuple	14, 15
9	ExprTuple	16, 17
10	ExprTuple	18, 19
11	Operation	operator: 69 operands: 20
12	ExprRange	lambda_map: 21 start_index: 102 end_index: 96
13	ExprRange	lambda_map: 22 start_index: 102 end_index: 91
14	ExprRange	lambda_map: 23 start_index: 102 end_index: 96
15	ExprRange	lambda_map: 23 start_index: 77 end_index: 78
16	ExprRange	lambda_map: 24 start_index: 102 end_index: 96
17	ExprRange	lambda_map: 25 start_index: 102 end_index: 91
18	ExprRange	lambda_map: 26 start_index: 102 end_index: 96
19	ExprRange	lambda_map: 27 start_index: 102 end_index: 91
20	ExprTuple	28, 71
21	Lambda	parameter: 76 body: 29
22	Lambda	parameter: 76 body: 30
23	Lambda	parameter: 76 body: 31
24	Lambda	parameter: 76 body: 32
25	Lambda	parameter: 76 body: 33
26	Lambda	parameter: 76 body: 34
27	Lambda	parameter: 76 body: 36
28	Operation	operator: 92 operands: 37
29	Operation	operator: 61 operands: 38
30	Operation	operator: 45 operands: 39
31	Operation	operator: 45 operands: 40
32	Operation	operator: 41 operands: 42
33	Operation	operator: 62 operands: 43
34	Operation	operator: 45 operands: 44
35	ExprTuple	76
36	Operation	operator: 45 operands: 46
37	ExprTuple	47, 102
38	NamedExprs	state: 48
39	NamedExprs	element: 49 targets: 57
40	NamedExprs	element: 50 targets: 51
41	Literal
42	NamedExprs	basis: 52
43	NamedExprs	operation: 53
44	NamedExprs	element: 54 targets: 55
45	Literal
46	NamedExprs	element: 56 targets: 57
47	Operation	operator: 100 operand: 71
48	Operation	operator: 59 operand: 72
49	Operation	operator: 61 operands: 68
50	Operation	operator: 62 operands: 63
51	Operation	operator: 69 operands: 64
52	Literal
53	Literal
54	Operation	operator: 67 operands: 65
55	Operation	operator: 69 operands: 66
56	Operation	operator: 67 operands: 68
57	Operation	operator: 69 operands: 70
58	ExprTuple	71
59	Literal
60	ExprTuple	72
61	Literal
62	Literal
63	NamedExprs	operation: 73 part: 76
64	ExprTuple	102, 78
65	NamedExprs	state: 74 part: 76
66	ExprTuple	102, 96
67	Literal
68	NamedExprs	state: 75 part: 76
69	Literal
70	ExprTuple	77, 78
71	Operation	operator: 79 operands: 80
72	Literal
73	Operation	operator: 81 operands: 82
74	Operation	operator: 83 operands: 84
75	Literal
76	Variable
77	Operation	operator: 92 operands: 85
78	Operation	operator: 92 operands: 86
79	Literal
80	ExprTuple	87, 88
81	Literal
82	ExprTuple	89, 96
83	Literal
84	ExprTuple	90, 96
85	ExprTuple	96, 102
86	ExprTuple	96, 91
87	Literal
88	Operation	operator: 92 operands: 93
89	Literal
90	Operation	operator: 94 operands: 95
91	Literal
92	Literal
93	ExprTuple	96, 97
94	Literal
95	ExprTuple	98, 99
96	Literal
97	Operation	operator: 100 operand: 102
98	Literal
99	Variable
100	Literal
101	ExprTuple	102
102	Literal

Expression of type Conditional¶

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

Expression of type Conditional ¶

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