logo

Expression of type InClass

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 k, m
from proveit.linear_algebra import ScalarMult, VecSum
from proveit.logic import InClass
from proveit.numbers import Exp, Mult, e, frac, i, one, pi, two
from proveit.physics.quantum import NumBra, NumKet, Qmult, QmultCodomain
from proveit.physics.quantum.QFT import InverseFourierTransform
from proveit.physics.quantum.QPE import _m_domain, _phase, _t
In [2]:
# build up the expression from sub-expressions
expr = InClass(Qmult(NumBra(m, _t), frac(one, Exp(two, frac(_t, two))), InverseFourierTransform(_t), VecSum(index_or_indices = [k], summand = ScalarMult(Exp(e, Mult(two, pi, i, _phase, k)), NumKet(k, _t)), domain = _m_domain)), QmultCodomain)
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({_{t}}\langle m \rvert \thinspace \frac{1}{2^{\frac{t}{2}}} \thinspace {\mathrm {FT}}^{\dag}_{t} \thinspace \left(\sum_{k=0}^{2^{t} - 1} \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi \cdot k} \cdot \lvert k \rangle_{t}\right)\right)\right) \underset{{\scriptscriptstyle c}}{\in} \mathcal{Q^*}
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: 5
operands: 6
4Literal
5Literal
6ExprTuple7, 8, 9, 10
7Operationoperator: 11
operands: 12
8Operationoperator: 27
operands: 13
9Operationoperator: 14
operand: 60
10Operationoperator: 16
operand: 20
11Literal
12ExprTuple18, 60
13ExprTuple61, 19
14Literal
15ExprTuple60
16Literal
17ExprTuple20
18Variable
19Operationoperator: 55
operands: 21
20Lambdaparameter: 52
body: 23
21ExprTuple59, 24
22ExprTuple52
23Conditionalvalue: 25
condition: 26
24Operationoperator: 27
operands: 28
25Operationoperator: 29
operands: 30
26Operationoperator: 31
operands: 32
27Literal
28ExprTuple60, 59
29Literal
30ExprTuple33, 34
31Literal
32ExprTuple52, 35
33Operationoperator: 55
operands: 36
34Operationoperator: 37
operands: 38
35Operationoperator: 39
operands: 40
36ExprTuple41, 42
37Literal
38ExprTuple52, 60
39Literal
40ExprTuple43, 44
41Literal
42Operationoperator: 45
operands: 46
43Literal
44Operationoperator: 47
operands: 48
45Literal
46ExprTuple59, 49, 50, 51, 52
47Literal
48ExprTuple53, 54
49Literal
50Literal
51Literal
52Variable
53Operationoperator: 55
operands: 56
54Operationoperator: 57
operand: 61
55Literal
56ExprTuple59, 60
57Literal
58ExprTuple61
59Literal
60Literal
61Literal