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 e, l
from proveit.logic import Equals
from proveit.numbers import Abs, Add, Exp, Interval, Neg, Sum, one, subtract, two
from proveit.physics.quantum.QPE import _neg_domain, _pos_domain, _rel_indexed_alpha, _two_pow__t_minus_one

In [2]:
# build up the expression from sub-expressions
sub_expr1 = [l]
sub_expr2 = Exp(Abs(_rel_indexed_alpha), two)
sub_expr3 = Sum(index_or_indices = sub_expr1, summand = sub_expr2, domain = _pos_domain)
expr = Equals(Add(Sum(index_or_indices = sub_expr1, summand = sub_expr2, domain = _neg_domain), sub_expr3), Add(Sum(index_or_indices = sub_expr1, summand = sub_expr2, domain = Interval(Add(Neg(_two_pow__t_minus_one), one), subtract(Neg(e), one))), sub_expr3))

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(\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) = \left(\left(\sum_{l = -2^{t - 1} + 1}^{-e - 1} \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)

In [5]:
stored_expr.style_options()

namedescriptiondefaultcurrent valuerelated methods
operation'infix' or 'function' style formattinginfixinfix
wrap_positionsposition(s) at which wrapping is to occur; '2 n - 1' is after the nth operand, '2 n' is after the nth operation.()()('with_wrapping_at', 'with_wrap_before_operator', 'with_wrap_after_operator', 'without_wrapping', 'wrap_positions')
justificationif any wrap positions are set, justify to the 'left', 'center', or 'right'centercenter('with_justification',)
directionDirection of the relation (normal or reversed)normalnormal('with_direction_reversed', 'is_reversed')
In [6]:
# display the expression information
stored_expr.expr_info()

core typesub-expressionsexpression
0Operationoperator: 1
operands: 2
1Literal
2ExprTuple3, 4
3Operationoperator: 66
operands: 5
4Operationoperator: 66
operands: 6
5ExprTuple7, 9
6ExprTuple8, 9
7Operationoperator: 12
operand: 14
8Operationoperator: 12
operand: 15
9Operationoperator: 12
operand: 16
10ExprTuple14
11ExprTuple15
12Literal
13ExprTuple16
14Lambdaparameter: 61
body: 17
15Lambdaparameter: 61
body: 18
16Lambdaparameter: 61
body: 20
17Conditionalvalue: 23
condition: 21
18Conditionalvalue: 23
condition: 22
19ExprTuple61
20Conditionalvalue: 23
condition: 24
21Operationoperator: 28
operands: 25
22Operationoperator: 28
operands: 26
23Operationoperator: 62
operands: 27
24Operationoperator: 28
operands: 29
25ExprTuple61, 30
26ExprTuple61, 31
27ExprTuple32, 64
28Literal
29ExprTuple61, 33
30Operationoperator: 38
operands: 34
31Operationoperator: 38
operands: 35
32Operationoperator: 36
operand: 43
33Operationoperator: 38
operands: 39
34ExprTuple41, 40
35ExprTuple41, 42
36Literal
37ExprTuple43
38Literal
39ExprTuple49, 58
40Operationoperator: 70
operand: 49
41Operationoperator: 66
operands: 45
42Operationoperator: 66
operands: 46
43Operationoperator: 47
operand: 52
44ExprTuple49
45ExprTuple50, 72
46ExprTuple51, 69
47Literal
48ExprTuple52
49Operationoperator: 66
operands: 53
50Operationoperator: 70
operand: 58
51Operationoperator: 70
operand: 59
52Operationoperator: 56
operands: 57
53ExprTuple59, 72
54ExprTuple58
55ExprTuple59
56Literal
57ExprTuple60, 61
58Operationoperator: 62
operands: 63
59Variable
60Literal
61Variable
62Literal
63ExprTuple64, 65
64Literal
65Operationoperator: 66
operands: 67
66Literal
67ExprTuple68, 69
68Literal
69Operationoperator: 70
operand: 72
70Literal
71ExprTuple72
72Literal