# 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.
# import Expression classes needed to build the expression
from proveit import Conditional, Lambda, e, l
from proveit.logic import Equals, InSet
from proveit.numbers import Abs, Add, Exp, Sum, two
from proveit.physics.quantum.QPE import Pfail, _e_domain, _neg_domain, _pos_domain, _rel_indexed_alpha

In [2]:
# build up the expression from sub-expressions
sub_expr1 = [l]
sub_expr2 = Exp(Abs(_rel_indexed_alpha), two)
expr = Lambda(e, Conditional(Equals(Pfail(e), Add(Sum(index_or_indices = sub_expr1, summand = sub_expr2, domain = _neg_domain), Sum(index_or_indices = sub_expr1, summand = sub_expr2, domain = _pos_domain))), 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(\left(\sum_{l = -2^{t - 1} + 1}^{-\left(e + 1\right)} \left|\alpha_{b_{\textit{f}} \oplus l}\right|^{2}\right) + \left(\sum_{l = e + 1}^{2^{t - 1}} \left|\alpha_{b_{\textit{f}} \oplus l}\right|^{2}\right)\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: 33
operands: 6
4Literal
5ExprTuple7, 8
6ExprTuple58, 9
7Operationoperator: 10
operand: 58
8Operationoperator: 65
operands: 12
9Operationoperator: 41
operands: 13
10Literal
11ExprTuple58
12ExprTuple14, 15
13ExprTuple71, 16
14Operationoperator: 18
operand: 21
15Operationoperator: 18
operand: 22
16Operationoperator: 65
operands: 20
17ExprTuple21
18Literal
19ExprTuple22
20ExprTuple57, 23
21Lambdaparameter: 60
body: 24
22Lambdaparameter: 60
body: 26
23Operationoperator: 69
operand: 63
24Conditionalvalue: 29
condition: 28
25ExprTuple60
26Conditionalvalue: 29
condition: 30
27ExprTuple63
28Operationoperator: 33
operands: 31
29Operationoperator: 61
operands: 32
30Operationoperator: 33
operands: 34
31ExprTuple60, 35
32ExprTuple36, 63
33Literal
34ExprTuple60, 37
35Operationoperator: 41
operands: 38
36Operationoperator: 39
operand: 45
37Operationoperator: 41
operands: 42
38ExprTuple43, 44
39Literal
40ExprTuple45
41Literal
42ExprTuple51, 57
43Operationoperator: 65
operands: 46
44Operationoperator: 69
operand: 51
45Operationoperator: 48
operand: 52
46ExprTuple50, 71
47ExprTuple51
48Literal
49ExprTuple52
50Operationoperator: 69
operand: 57
51Operationoperator: 65
operands: 54
52Operationoperator: 55
operands: 56
53ExprTuple57
54ExprTuple58, 71
55Literal
56ExprTuple59, 60
57Operationoperator: 61
operands: 62
58Variable
59Literal
60Variable
61Literal
62ExprTuple63, 64
63Literal
64Operationoperator: 65
operands: 66
65Literal
66ExprTuple67, 68
67Literal
68Operationoperator: 69
operand: 71
69Literal
70ExprTuple71
71Literal