logo

Expression of type Conditional

from the theory of proveit.physics.quantum.QPE

In [1]:
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, ModAbs, greater, 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
In [2]:
# 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))), greater(ModAbs(subtract(m, Literal("b_{f}", latex_format = r"b_{\textit{f}}", theory = "proveit.physics.quantum.QPE")), sub_expr4), e)))
expr:
In [3]:
# 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
In [4]:
# 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}} > e\right..
In [5]:
stored_expr.style_options()
namedescriptiondefaultcurrent valuerelated methods
condition_delimiter'comma' or 'and'commacomma('with_comma_delimiter', 'with_conjunction_delimiter')
In [6]:
# display the expression information
stored_expr.expr_info()
 core typesub-expressionsexpression
0Conditionalvalue: 1
condition: 2
1Operationoperator: 3
operands: 4
2Operationoperator: 5
operands: 6
3Literal
4ExprTuple7, 8, 9, 10
5Literal
6ExprTuple11, 12
7ExprTuple13, 14
8ExprTuple15, 16
9ExprTuple17, 18
10ExprTuple19, 20
11Operationoperator: 21
operands: 22
12Operationoperator: 23
operands: 24
13ExprRangelambda_map: 25
start_index: 108
end_index: 109
14ExprRangelambda_map: 26
start_index: 108
end_index: 110
15ExprRangelambda_map: 27
start_index: 108
end_index: 109
16ExprRangelambda_map: 27
start_index: 90
end_index: 91
17ExprRangelambda_map: 28
start_index: 108
end_index: 109
18ExprRangelambda_map: 29
start_index: 108
end_index: 110
19ExprRangelambda_map: 30
start_index: 108
end_index: 109
20ExprRangelambda_map: 31
start_index: 108
end_index: 110
21Literal
22ExprTuple107, 32
23Literal
24ExprTuple33, 34
25Lambdaparameter: 89
body: 35
26Lambdaparameter: 89
body: 36
27Lambdaparameter: 89
body: 37
28Lambdaparameter: 89
body: 38
29Lambdaparameter: 89
body: 39
30Lambdaparameter: 89
body: 40
31Lambdaparameter: 89
body: 42
32Operationoperator: 80
operands: 43
33Variable
34Operationoperator: 44
operands: 45
35Operationoperator: 72
operands: 46
36Operationoperator: 53
operands: 47
37Operationoperator: 53
operands: 48
38Operationoperator: 49
operands: 50
39Operationoperator: 73
operands: 51
40Operationoperator: 53
operands: 52
41ExprTuple89
42Operationoperator: 53
operands: 54
43ExprTuple55, 56
44Literal
45ExprTuple57, 82
46NamedExprsstate: 58
47NamedExprselement: 59
targets: 67
48NamedExprselement: 60
targets: 61
49Literal
50NamedExprsbasis: 62
51NamedExprsoperation: 63
52NamedExprselement: 64
targets: 65
53Literal
54NamedExprselement: 66
targets: 67
55Literal
56Operationoperator: 102
operands: 68
57Operationoperator: 102
operands: 69
58Operationoperator: 70
operand: 85
59Operationoperator: 72
operands: 79
60Operationoperator: 73
operands: 74
61Operationoperator: 80
operands: 75
62Literal
63Literal
64Operationoperator: 78
operands: 76
65Operationoperator: 80
operands: 77
66Operationoperator: 78
operands: 79
67Operationoperator: 80
operands: 81
68ExprTuple82, 83
69ExprTuple107, 84
70Literal
71ExprTuple85
72Literal
73Literal
74NamedExprsoperation: 86
part: 89
75ExprTuple108, 91
76NamedExprsstate: 87
part: 89
77ExprTuple108, 109
78Literal
79NamedExprsstate: 88
part: 89
80Literal
81ExprTuple90, 91
82Operationoperator: 92
operands: 93
83Operationoperator: 95
operand: 108
84Operationoperator: 95
operand: 105
85Literal
86Operationoperator: 97
operands: 98
87Operationoperator: 99
operands: 100
88Literal
89Variable
90Operationoperator: 102
operands: 101
91Operationoperator: 102
operands: 103
92Literal
93ExprTuple104, 109
94ExprTuple108
95Literal
96ExprTuple105
97Literal
98ExprTuple106, 109
99Literal
100ExprTuple107, 109
101ExprTuple109, 108
102Literal
103ExprTuple109, 110
104Literal
105Literal
106Literal
107Variable
108Literal
109Literal
110Literal