# 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, 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 = 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())

\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()

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: 32
operands: 5
3Literal
4ExprTuple6, 7
5ExprTuple57, 8
6Operationoperator: 9
operand: 57
7Operationoperator: 64
operands: 11
8Operationoperator: 40
operands: 12
9Literal
10ExprTuple57
11ExprTuple13, 14
12ExprTuple70, 15
13Operationoperator: 17
operand: 20
14Operationoperator: 17
operand: 21
15Operationoperator: 64
operands: 19
16ExprTuple20
17Literal
18ExprTuple21
19ExprTuple56, 22
20Lambdaparameter: 59
body: 23
21Lambdaparameter: 59
body: 25
22Operationoperator: 68
operand: 62
23Conditionalvalue: 28
condition: 27
24ExprTuple59
25Conditionalvalue: 28
condition: 29
26ExprTuple62
27Operationoperator: 32
operands: 30
28Operationoperator: 60
operands: 31
29Operationoperator: 32
operands: 33
30ExprTuple59, 34
31ExprTuple35, 62
32Literal
33ExprTuple59, 36
34Operationoperator: 40
operands: 37
35Operationoperator: 38
operand: 44
36Operationoperator: 40
operands: 41
37ExprTuple42, 43
38Literal
39ExprTuple44
40Literal
41ExprTuple50, 56
42Operationoperator: 64
operands: 45
43Operationoperator: 68
operand: 50
44Operationoperator: 47
operand: 51
45ExprTuple49, 70
46ExprTuple50
47Literal
48ExprTuple51
49Operationoperator: 68
operand: 56
50Operationoperator: 64
operands: 53
51Operationoperator: 54
operands: 55
52ExprTuple56
53ExprTuple57, 70
54Literal
55ExprTuple58, 59
56Operationoperator: 60
operands: 61
57Variable
58Literal
59Variable
60Literal
61ExprTuple62, 63
62Literal
63Operationoperator: 64
operands: 65
64Literal
65ExprTuple66, 67
66Literal
67Operationoperator: 68
operand: 70
68Literal
69ExprTuple70
70Literal