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, Literal, Variable, VertExprArray, e, m
from proveit.logic import And, InSet
from proveit.numbers import Add, Exp, Interval, LessEq, ModAbs, one, subtract, two, zero
from proveit.physics.quantum import I, NumKet, Z, ket_plus
from proveit.physics.quantum.QPE import QPE
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(Literal("t", theory = "proveit.physics.quantum.QPE"), one)
sub_expr3 = Add(Literal("t", theory = "proveit.physics.quantum.QPE"), Literal("s", theory = "proveit.physics.quantum.QPE"))
sub_expr4 = Exp(two, Literal("t", theory = "proveit.physics.quantum.QPE"))
sub_expr5 = Interval(sub_expr2, sub_expr3)
sub_expr6 = MultiQubitElem(element = Gate(operation = QPE(Literal("U", theory = "proveit.physics.quantum.QPE"), Literal("t", theory = "proveit.physics.quantum.QPE")), part = sub_expr1), targets = Interval(one, sub_expr3))
expr = Conditional(Qcircuit(vert_expr_array = VertExprArray([ExprRange(sub_expr1, Input(state = ket_plus), one, Literal("t", theory = "proveit.physics.quantum.QPE")), ExprRange(sub_expr1, MultiQubitElem(element = Input(state = Literal("|u>", latex_format = r"\lvert u \rangle", theory = "proveit.physics.quantum.QPE"), part = sub_expr1), targets = sub_expr5), one, Literal("s", theory = "proveit.physics.quantum.QPE"))], [ExprRange(sub_expr1, sub_expr6, one, Literal("t", theory = "proveit.physics.quantum.QPE")), ExprRange(sub_expr1, sub_expr6, sub_expr2, sub_expr3)], [ExprRange(sub_expr1, Measure(basis = Z), one, Literal("t", theory = "proveit.physics.quantum.QPE")), ExprRange(sub_expr1, Gate(operation = I).with_implicit_representation(), one, Literal("s", theory = "proveit.physics.quantum.QPE"))], [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(m, Literal("t", theory = "proveit.physics.quantum.QPE")), part = sub_expr1), targets = Interval(one, Literal("t", theory = "proveit.physics.quantum.QPE"))), one, Literal("t", theory = "proveit.physics.quantum.QPE")), ExprRange(sub_expr1, MultiQubitElem(element = Output(state = Literal("|u>", latex_format = r"\lvert u \rangle", theory = "proveit.physics.quantum.QPE"), part = sub_expr1), targets = sub_expr5), one, Literal("s", theory = "proveit.physics.quantum.QPE"))])), And(InSet(m, Interval(zero, subtract(sub_expr4, one))), LessEq(ModAbs(subtract(m, Literal("b_{f}", latex_format = r"b_{\textit{f}}", theory = "proveit.physics.quantum.QPE")), sub_expr4), e)))

# 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 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} \textrm{ if } m \in \{0~\ldotp \ldotp~2^{t} - 1\} ,  \left|m - b_{\textit{f}}\right|_{\textup{mod}\thinspace 2^{t}} \leq e\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	11, 12
7	ExprTuple	13, 14
8	ExprTuple	15, 16
9	ExprTuple	17, 18
10	ExprTuple	19, 20
11	Operation	operator: 21 operands: 22
12	Operation	operator: 23 operands: 24
13	ExprRange	lambda_map: 25 start_index: 108 end_index: 109
14	ExprRange	lambda_map: 26 start_index: 108 end_index: 110
15	ExprRange	lambda_map: 27 start_index: 108 end_index: 109
16	ExprRange	lambda_map: 27 start_index: 90 end_index: 91
17	ExprRange	lambda_map: 28 start_index: 108 end_index: 109
18	ExprRange	lambda_map: 29 start_index: 108 end_index: 110
19	ExprRange	lambda_map: 30 start_index: 108 end_index: 109
20	ExprRange	lambda_map: 31 start_index: 108 end_index: 110
21	Literal
22	ExprTuple	107, 32
23	Literal
24	ExprTuple	33, 34
25	Lambda	parameter: 89 body: 35
26	Lambda	parameter: 89 body: 36
27	Lambda	parameter: 89 body: 37
28	Lambda	parameter: 89 body: 38
29	Lambda	parameter: 89 body: 39
30	Lambda	parameter: 89 body: 40
31	Lambda	parameter: 89 body: 42
32	Operation	operator: 80 operands: 43
33	Operation	operator: 44 operands: 45
34	Variable
35	Operation	operator: 72 operands: 46
36	Operation	operator: 53 operands: 47
37	Operation	operator: 53 operands: 48
38	Operation	operator: 49 operands: 50
39	Operation	operator: 73 operands: 51
40	Operation	operator: 53 operands: 52
41	ExprTuple	89
42	Operation	operator: 53 operands: 54
43	ExprTuple	55, 56
44	Literal
45	ExprTuple	57, 82
46	NamedExprs	state: 58
47	NamedExprs	element: 59 targets: 67
48	NamedExprs	element: 60 targets: 61
49	Literal
50	NamedExprs	basis: 62
51	NamedExprs	operation: 63
52	NamedExprs	element: 64 targets: 65
53	Literal
54	NamedExprs	element: 66 targets: 67
55	Literal
56	Operation	operator: 102 operands: 68
57	Operation	operator: 102 operands: 69
58	Operation	operator: 70 operand: 85
59	Operation	operator: 72 operands: 79
60	Operation	operator: 73 operands: 74
61	Operation	operator: 80 operands: 75
62	Literal
63	Literal
64	Operation	operator: 78 operands: 76
65	Operation	operator: 80 operands: 77
66	Operation	operator: 78 operands: 79
67	Operation	operator: 80 operands: 81
68	ExprTuple	82, 83
69	ExprTuple	107, 84
70	Literal
71	ExprTuple	85
72	Literal
73	Literal
74	NamedExprs	operation: 86 part: 89
75	ExprTuple	108, 91
76	NamedExprs	state: 87 part: 89
77	ExprTuple	108, 109
78	Literal
79	NamedExprs	state: 88 part: 89
80	Literal
81	ExprTuple	90, 91
82	Operation	operator: 92 operands: 93
83	Operation	operator: 95 operand: 108
84	Operation	operator: 95 operand: 105
85	Literal
86	Operation	operator: 97 operands: 98
87	Operation	operator: 99 operands: 100
88	Literal
89	Variable
90	Operation	operator: 102 operands: 101
91	Operation	operator: 102 operands: 103
92	Literal
93	ExprTuple	104, 109
94	ExprTuple	108
95	Literal
96	ExprTuple	105
97	Literal
98	ExprTuple	106, 109
99	Literal
100	ExprTuple	107, 109
101	ExprTuple	109, 108
102	Literal
103	ExprTuple	109, 110
104	Literal
105	Literal
106	Literal
107	Variable
108	Literal
109	Literal
110	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 ¶