logo

Expression of type Lambda

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, Lambda, 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 = Lambda(m, 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())
m \mapsto \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()
no style options
In [6]:
# display the expression information
stored_expr.expr_info()
 core typesub-expressionsexpression
0Lambdaparameter: 109
body: 2
1ExprTuple109
2Conditionalvalue: 3
condition: 4
3Operationoperator: 5
operands: 6
4Operationoperator: 7
operands: 8
5Literal
6ExprTuple9, 10, 11, 12
7Literal
8ExprTuple13, 14
9ExprTuple15, 16
10ExprTuple17, 18
11ExprTuple19, 20
12ExprTuple21, 22
13Operationoperator: 23
operands: 24
14Operationoperator: 25
operands: 26
15ExprRangelambda_map: 27
start_index: 110
end_index: 111
16ExprRangelambda_map: 28
start_index: 110
end_index: 112
17ExprRangelambda_map: 29
start_index: 110
end_index: 111
18ExprRangelambda_map: 29
start_index: 92
end_index: 93
19ExprRangelambda_map: 30
start_index: 110
end_index: 111
20ExprRangelambda_map: 31
start_index: 110
end_index: 112
21ExprRangelambda_map: 32
start_index: 110
end_index: 111
22ExprRangelambda_map: 33
start_index: 110
end_index: 112
23Literal
24ExprTuple109, 34
25Literal
26ExprTuple35, 36
27Lambdaparameter: 91
body: 37
28Lambdaparameter: 91
body: 38
29Lambdaparameter: 91
body: 39
30Lambdaparameter: 91
body: 40
31Lambdaparameter: 91
body: 41
32Lambdaparameter: 91
body: 42
33Lambdaparameter: 91
body: 44
34Operationoperator: 82
operands: 45
35Variable
36Operationoperator: 46
operands: 47
37Operationoperator: 74
operands: 48
38Operationoperator: 55
operands: 49
39Operationoperator: 55
operands: 50
40Operationoperator: 51
operands: 52
41Operationoperator: 75
operands: 53
42Operationoperator: 55
operands: 54
43ExprTuple91
44Operationoperator: 55
operands: 56
45ExprTuple57, 58
46Literal
47ExprTuple59, 84
48NamedExprsstate: 60
49NamedExprselement: 61
targets: 69
50NamedExprselement: 62
targets: 63
51Literal
52NamedExprsbasis: 64
53NamedExprsoperation: 65
54NamedExprselement: 66
targets: 67
55Literal
56NamedExprselement: 68
targets: 69
57Literal
58Operationoperator: 104
operands: 70
59Operationoperator: 104
operands: 71
60Operationoperator: 72
operand: 87
61Operationoperator: 74
operands: 81
62Operationoperator: 75
operands: 76
63Operationoperator: 82
operands: 77
64Literal
65Literal
66Operationoperator: 80
operands: 78
67Operationoperator: 82
operands: 79
68Operationoperator: 80
operands: 81
69Operationoperator: 82
operands: 83
70ExprTuple84, 85
71ExprTuple109, 86
72Literal
73ExprTuple87
74Literal
75Literal
76NamedExprsoperation: 88
part: 91
77ExprTuple110, 93
78NamedExprsstate: 89
part: 91
79ExprTuple110, 111
80Literal
81NamedExprsstate: 90
part: 91
82Literal
83ExprTuple92, 93
84Operationoperator: 94
operands: 95
85Operationoperator: 97
operand: 110
86Operationoperator: 97
operand: 107
87Literal
88Operationoperator: 99
operands: 100
89Operationoperator: 101
operands: 102
90Literal
91Variable
92Operationoperator: 104
operands: 103
93Operationoperator: 104
operands: 105
94Literal
95ExprTuple106, 111
96ExprTuple110
97Literal
98ExprTuple107
99Literal
100ExprTuple108, 111
101Literal
102ExprTuple109, 111
103ExprTuple111, 110
104Literal
105ExprTuple111, 112
106Literal
107Literal
108Literal
109Variable
110Literal
111Literal
112Literal