# 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 Lambda, m
from proveit.logic import InSet, Surjections
from proveit.physics.quantum.QPE import _Omega, _m_domain, _phase_est_circuit

In [2]:
# build up the expression from sub-expressions
expr = InSet(Lambda(m, _phase_est_circuit), Surjections(_m_domain, _Omega))

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[m \mapsto \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)\right] \in \left[\{0~\ldotp \ldotp~2^{t} - 1\} \xrightarrow[\text{onto}]{} \Omega\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
3Lambdaparameter: 97
body: 6
4Operationoperator: 7
operands: 8
5ExprTuple97
6Operationoperator: 9
operands: 10
7Literal
8ExprTuple11, 12
9Literal
10ExprTuple13, 14, 15, 16
11Operationoperator: 80
operands: 17
12Literal
13ExprTuple18, 19
14ExprTuple20, 21
15ExprTuple22, 23
16ExprTuple24, 25
17ExprTuple26, 27
18ExprRangelambda_map: 28
start_index: 98
end_index: 99
19ExprRangelambda_map: 29
start_index: 98
end_index: 100
20ExprRangelambda_map: 30
start_index: 98
end_index: 99
21ExprRangelambda_map: 30
start_index: 87
end_index: 88
22ExprRangelambda_map: 31
start_index: 98
end_index: 99
23ExprRangelambda_map: 32
start_index: 98
end_index: 100
24ExprRangelambda_map: 33
start_index: 98
end_index: 99
25ExprRangelambda_map: 34
start_index: 98
end_index: 100
26Literal
27Operationoperator: 94
operands: 35
28Lambdaparameter: 86
body: 36
29Lambdaparameter: 86
body: 37
30Lambdaparameter: 86
body: 38
31Lambdaparameter: 86
body: 39
32Lambdaparameter: 86
body: 40
33Lambdaparameter: 86
body: 41
34Lambdaparameter: 86
body: 43
35ExprTuple44, 45
36Operationoperator: 72
operands: 46
37Operationoperator: 53
operands: 47
38Operationoperator: 53
operands: 48
39Operationoperator: 49
operands: 50
40Operationoperator: 73
operands: 51
41Operationoperator: 53
operands: 52
42ExprTuple86
43Operationoperator: 53
operands: 54
44Operationoperator: 55
operands: 56
45Operationoperator: 57
operand: 98
47NamedExprselement: 60
targets: 68
48NamedExprselement: 61
targets: 62
49Literal
50NamedExprsbasis: 63
51NamedExprsoperation: 64
52NamedExprselement: 65
targets: 66
53Literal
54NamedExprselement: 67
targets: 68
55Literal
56ExprTuple69, 99
57Literal
58ExprTuple98
59Operationoperator: 70
operand: 82
60Operationoperator: 72
operands: 79
61Operationoperator: 73
operands: 74
62Operationoperator: 80
operands: 75
63Literal
64Literal
65Operationoperator: 78
operands: 76
66Operationoperator: 80
operands: 77
67Operationoperator: 78
operands: 79
68Operationoperator: 80
operands: 81
69Literal
70Literal
71ExprTuple82
72Literal
73Literal
74NamedExprsoperation: 83
part: 86
75ExprTuple98, 88
part: 86
77ExprTuple98, 99
78Literal
part: 86
80Literal
81ExprTuple87, 88
82Literal
83Operationoperator: 89
operands: 90
84Operationoperator: 91
operands: 92
85Literal
86Variable
87Operationoperator: 94
operands: 93
88Operationoperator: 94
operands: 95
89Literal
90ExprTuple96, 99
91Literal
92ExprTuple97, 99
93ExprTuple99, 98
94Literal
95ExprTuple99, 100
96Literal
97Variable
98Literal
99Literal
100Literal