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

In [2]:
# build up the expression from sub-expressions
expr = ExprTuple(Lambda(m, _phase_est_circuit), Bijections(_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), \left[\{0~\ldotp \ldotp~2^{t} - 1\} \xrightarrow[\text{onto}]{\text{1-to-1}} \Omega\right]\right)

In [5]:
stored_expr.style_options()

namedescriptiondefaultcurrent valuerelated methods
wrap_positionsposition(s) at which wrapping is to occur; 'n' is after the nth comma.()()('with_wrapping_at',)
justificationif any wrap positions are set, justify to the 'left', 'center', or 'right'leftleft('with_justification',)
In [6]:
# display the expression information
stored_expr.expr_info()

core typesub-expressionsexpression
0ExprTuple1, 2
1Lambdaparameter: 95
body: 4
2Operationoperator: 5
operands: 6
3ExprTuple95
4Operationoperator: 7
operands: 8
5Literal
6ExprTuple9, 10
7Literal
8ExprTuple11, 12, 13, 14
9Operationoperator: 78
operands: 15
10Literal
11ExprTuple16, 17
12ExprTuple18, 19
13ExprTuple20, 21
14ExprTuple22, 23
15ExprTuple24, 25
16ExprRangelambda_map: 26
start_index: 96
end_index: 97
17ExprRangelambda_map: 27
start_index: 96
end_index: 98
18ExprRangelambda_map: 28
start_index: 96
end_index: 97
19ExprRangelambda_map: 28
start_index: 85
end_index: 86
20ExprRangelambda_map: 29
start_index: 96
end_index: 97
21ExprRangelambda_map: 30
start_index: 96
end_index: 98
22ExprRangelambda_map: 31
start_index: 96
end_index: 97
23ExprRangelambda_map: 32
start_index: 96
end_index: 98
24Literal
25Operationoperator: 92
operands: 33
26Lambdaparameter: 84
body: 34
27Lambdaparameter: 84
body: 35
28Lambdaparameter: 84
body: 36
29Lambdaparameter: 84
body: 37
30Lambdaparameter: 84
body: 38
31Lambdaparameter: 84
body: 39
32Lambdaparameter: 84
body: 41
33ExprTuple42, 43
34Operationoperator: 70
operands: 44
35Operationoperator: 51
operands: 45
36Operationoperator: 51
operands: 46
37Operationoperator: 47
operands: 48
38Operationoperator: 71
operands: 49
39Operationoperator: 51
operands: 50
40ExprTuple84
41Operationoperator: 51
operands: 52
42Operationoperator: 53
operands: 54
43Operationoperator: 55
operand: 96
45NamedExprselement: 58
targets: 66
46NamedExprselement: 59
targets: 60
47Literal
48NamedExprsbasis: 61
49NamedExprsoperation: 62
50NamedExprselement: 63
targets: 64
51Literal
52NamedExprselement: 65
targets: 66
53Literal
54ExprTuple67, 97
55Literal
56ExprTuple96
57Operationoperator: 68
operand: 80
58Operationoperator: 70
operands: 77
59Operationoperator: 71
operands: 72
60Operationoperator: 78
operands: 73
61Literal
62Literal
63Operationoperator: 76
operands: 74
64Operationoperator: 78
operands: 75
65Operationoperator: 76
operands: 77
66Operationoperator: 78
operands: 79
67Literal
68Literal
69ExprTuple80
70Literal
71Literal
72NamedExprsoperation: 81
part: 84
73ExprTuple96, 86
part: 84
75ExprTuple96, 97
76Literal
part: 84
78Literal
79ExprTuple85, 86
80Literal
81Operationoperator: 87
operands: 88
82Operationoperator: 89
operands: 90
83Literal
84Variable
85Operationoperator: 92
operands: 91
86Operationoperator: 92
operands: 93
87Literal
88ExprTuple94, 97
89Literal
90ExprTuple95, 97
91ExprTuple97, 96
92Literal
93ExprTuple97, 98
94Literal
95Variable
96Literal
97Literal
98Literal