# 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.logic import Equals
from proveit.physics.quantum.QPE import _Omega, _sample_space

In [2]:
# build up the expression from sub-expressions
expr = Equals(_Omega, _sample_space)

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

\Omega = \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\}_{m \in \{0~\ldotp \ldotp~2^{t} - 1\}}

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
3Literal
4Operationoperator: 5
operand: 7
5Literal
6ExprTuple7
7Lambdaparameter: 101
body: 9
8ExprTuple101
9Conditionalvalue: 10
condition: 11
10Operationoperator: 12
operands: 13
11Operationoperator: 14
operands: 15
12Literal
13ExprTuple16, 17, 18, 19
14Literal
15ExprTuple101, 20
16ExprTuple21, 22
17ExprTuple23, 24
18ExprTuple25, 26
19ExprTuple27, 28
20Operationoperator: 83
operands: 29
21ExprRangelambda_map: 30
start_index: 102
end_index: 103
22ExprRangelambda_map: 31
start_index: 102
end_index: 104
23ExprRangelambda_map: 32
start_index: 102
end_index: 103
24ExprRangelambda_map: 32
start_index: 91
end_index: 92
25ExprRangelambda_map: 33
start_index: 102
end_index: 103
26ExprRangelambda_map: 34
start_index: 102
end_index: 104
27ExprRangelambda_map: 35
start_index: 102
end_index: 103
28ExprRangelambda_map: 36
start_index: 102
end_index: 104
29ExprTuple37, 38
30Lambdaparameter: 90
body: 39
31Lambdaparameter: 90
body: 40
32Lambdaparameter: 90
body: 41
33Lambdaparameter: 90
body: 42
34Lambdaparameter: 90
body: 43
35Lambdaparameter: 90
body: 44
36Lambdaparameter: 90
body: 46
37Literal
38Operationoperator: 98
operands: 47
39Operationoperator: 75
operands: 48
40Operationoperator: 55
operands: 49
41Operationoperator: 55
operands: 50
42Operationoperator: 51
operands: 52
43Operationoperator: 76
operands: 53
44Operationoperator: 55
operands: 54
45ExprTuple90
46Operationoperator: 55
operands: 56
47ExprTuple57, 58
49NamedExprselement: 60
targets: 68
50NamedExprselement: 61
targets: 62
51Literal
52NamedExprsbasis: 63
53NamedExprsoperation: 64
54NamedExprselement: 65
targets: 66
55Literal
56NamedExprselement: 67
targets: 68
57Operationoperator: 69
operands: 70
58Operationoperator: 71
operand: 102
59Operationoperator: 73
operand: 86
60Operationoperator: 75
operands: 82
61Operationoperator: 76
operands: 77
62Operationoperator: 83
operands: 78
63Literal
64Literal
65Operationoperator: 81
operands: 79
66Operationoperator: 83
operands: 80
67Operationoperator: 81
operands: 82
68Operationoperator: 83
operands: 84
69Literal
70ExprTuple85, 103
71Literal
72ExprTuple102
73Literal
74ExprTuple86
75Literal
76Literal
77NamedExprsoperation: 87
part: 90
78ExprTuple102, 92
part: 90
80ExprTuple102, 103
81Literal
part: 90
83Literal
84ExprTuple91, 92
85Literal
86Literal
87Operationoperator: 93
operands: 94
88Operationoperator: 95
operands: 96
89Literal
90Variable
91Operationoperator: 98
operands: 97
92Operationoperator: 98
operands: 99
93Literal
94ExprTuple100, 103
95Literal
96ExprTuple101, 103
97ExprTuple103, 102
98Literal
99ExprTuple103, 104
100Literal
101Variable
102Literal
103Literal
104Literal