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, Lambda, e
from proveit.logic import Equals, InSet
from proveit.physics.quantum.QPE import Pfail, _e_domain, _fail_prob_e
In [2]:
# build up the expression from sub-expressions
expr = Lambda(e, Conditional(Equals(Pfail(e), _fail_prob_e), InSet(e, _e_domain)))
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())
e \mapsto \left\{\left[P_{\rm fail}\right]\left(e\right) = \left[\begin{array}{l}\textrm{Prob}_{m \in \{0~\ldotp \ldotp~2^{t} - 1\}~|~\left|m - b_{\textit{f}}\right|_{\textup{mod}\thinspace 2^{t}} > e}~\\
\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}\right)\end{array}\right] \textrm{ if } e \in \{1~\ldotp \ldotp~2^{t - 1} - 2\}\right..
In [5]:
stored_expr.style_options()
no style options
In [6]:
# display the expression information
stored_expr.expr_info()
 core typesub-expressionsexpression
0Lambdaparameter: 58
body: 1
1Conditionalvalue: 2
condition: 3
2Operationoperator: 4
operands: 5
3Operationoperator: 45
operands: 6
4Literal
5ExprTuple7, 8
6ExprTuple58, 9
7Operationoperator: 10
operand: 58
8Operationoperator: 12
operand: 15
9Operationoperator: 105
operands: 14
10Literal
11ExprTuple58
12Literal
13ExprTuple15
14ExprTuple133, 16
15Lambdaparameter: 132
body: 18
16Operationoperator: 127
operands: 19
17ExprTuple132
18Conditionalvalue: 20
condition: 21
19ExprTuple22, 23
20Operationoperator: 24
operands: 25
21Operationoperator: 26
operands: 27
22Operationoperator: 117
operands: 28
23Operationoperator: 120
operand: 129
24Literal
25ExprTuple30, 31, 32, 33
26Literal
27ExprTuple34, 35
28ExprTuple129, 36
29ExprTuple129
30ExprTuple37, 38
31ExprTuple39, 40
32ExprTuple41, 42
33ExprTuple43, 44
34Operationoperator: 45
operands: 46
35Operationoperator: 47
operands: 48
36Operationoperator: 127
operands: 49
37ExprRangelambda_map: 50
start_index: 133
end_index: 134
38ExprRangelambda_map: 51
start_index: 133
end_index: 135
39ExprRangelambda_map: 52
start_index: 133
end_index: 134
40ExprRangelambda_map: 52
start_index: 115
end_index: 116
41ExprRangelambda_map: 53
start_index: 133
end_index: 134
42ExprRangelambda_map: 54
start_index: 133
end_index: 135
43ExprRangelambda_map: 55
start_index: 133
end_index: 134
44ExprRangelambda_map: 56
start_index: 133
end_index: 135
45Literal
46ExprTuple132, 57
47Literal
48ExprTuple58, 59
49ExprTuple134, 108
50Lambdaparameter: 114
body: 60
51Lambdaparameter: 114
body: 61
52Lambdaparameter: 114
body: 62
53Lambdaparameter: 114
body: 63
54Lambdaparameter: 114
body: 64
55Lambdaparameter: 114
body: 65
56Lambdaparameter: 114
body: 67
57Operationoperator: 105
operands: 68
58Variable
59Operationoperator: 69
operands: 70
60Operationoperator: 97
operands: 71
61Operationoperator: 78
operands: 72
62Operationoperator: 78
operands: 73
63Operationoperator: 74
operands: 75
64Operationoperator: 98
operands: 76
65Operationoperator: 78
operands: 77
66ExprTuple114
67Operationoperator: 78
operands: 79
68ExprTuple80, 81
69Literal
70ExprTuple82, 107
71NamedExprsstate: 83
72NamedExprselement: 84
targets: 92
73NamedExprselement: 85
targets: 86
74Literal
75NamedExprsbasis: 87
76NamedExprsoperation: 88
77NamedExprselement: 89
targets: 90
78Literal
79NamedExprselement: 91
targets: 92
80Literal
81Operationoperator: 127
operands: 93
82Operationoperator: 127
operands: 94
83Operationoperator: 95
operand: 110
84Operationoperator: 97
operands: 104
85Operationoperator: 98
operands: 99
86Operationoperator: 105
operands: 100
87Literal
88Literal
89Operationoperator: 103
operands: 101
90Operationoperator: 105
operands: 102
91Operationoperator: 103
operands: 104
92Operationoperator: 105
operands: 106
93ExprTuple107, 108
94ExprTuple132, 109
95Literal
96ExprTuple110
97Literal
98Literal
99NamedExprsoperation: 111
part: 114
100ExprTuple133, 116
101NamedExprsstate: 112
part: 114
102ExprTuple133, 134
103Literal
104NamedExprsstate: 113
part: 114
105Literal
106ExprTuple115, 116
107Operationoperator: 117
operands: 118
108Operationoperator: 120
operand: 133
109Operationoperator: 120
operand: 130
110Literal
111Operationoperator: 122
operands: 123
112Operationoperator: 124
operands: 125
113Literal
114Variable
115Operationoperator: 127
operands: 126
116Operationoperator: 127
operands: 128
117Literal
118ExprTuple129, 134
119ExprTuple133
120Literal
121ExprTuple130
122Literal
123ExprTuple131, 134
124Literal
125ExprTuple132, 134
126ExprTuple134, 133
127Literal
128ExprTuple134, 135
129Literal
130Literal
131Literal
132Variable
133Literal
134Literal
135Literal