# 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, l, m
from proveit.logic import Bijections, InSet
from proveit.physics.quantum.QPE import _Omega, _b_floor, _full_domain, _m_domain, _phase_est_circuit, _two_pow_t

In [2]:
# build up the expression from sub-expressions
expr = ExprTuple(InSet(Lambda(l, Mod(Add(_b_floor, l), _two_pow_t)), Bijections(_full_domain, _m_domain)), InSet(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(\left[l \mapsto \left(\left(b_{\textit{f}} + l\right) ~\textup{mod}~ 2^{t}\right)\right] \in \left[\{-2^{t - 1} + 1~\ldotp \ldotp~2^{t - 1}\} \xrightarrow[\text{onto}]{\text{1-to-1}} \{0~\ldotp \ldotp~2^{t} - 1\}\right], \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}]{\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
1Operationoperator: 4
operands: 3
2Operationoperator: 4
operands: 5
3ExprTuple6, 7
4Literal
5ExprTuple8, 9
6Lambdaparameter: 44
body: 11
7Operationoperator: 15
operands: 12
8Lambdaparameter: 119
body: 14
9Operationoperator: 15
operands: 16
10ExprTuple44
11Operationoperator: 17
operands: 18
12ExprTuple19, 22
13ExprTuple119
14Operationoperator: 20
operands: 21
15Literal
16ExprTuple22, 23
17Literal
18ExprTuple24, 63
19Operationoperator: 98
operands: 25
20Literal
21ExprTuple26, 27, 28, 29
22Operationoperator: 98
operands: 30
23Literal
24Operationoperator: 115
operands: 31
25ExprTuple32, 75
26ExprTuple33, 34
27ExprTuple35, 36
28ExprTuple37, 38
29ExprTuple39, 40
30ExprTuple41, 42
31ExprTuple43, 44
32Operationoperator: 115
operands: 45
33ExprRangelambda_map: 46
start_index: 124
end_index: 120
34ExprRangelambda_map: 47
start_index: 124
end_index: 121
35ExprRangelambda_map: 48
start_index: 124
end_index: 120
36ExprRangelambda_map: 48
start_index: 107
end_index: 108
37ExprRangelambda_map: 49
start_index: 124
end_index: 120
38ExprRangelambda_map: 50
start_index: 124
end_index: 121
39ExprRangelambda_map: 51
start_index: 124
end_index: 120
40ExprRangelambda_map: 52
start_index: 124
end_index: 121
41Literal
42Operationoperator: 115
operands: 53
43Literal
44Variable
45ExprTuple54, 124
46Lambdaparameter: 106
body: 55
47Lambdaparameter: 106
body: 56
48Lambdaparameter: 106
body: 57
49Lambdaparameter: 106
body: 58
50Lambdaparameter: 106
body: 59
51Lambdaparameter: 106
body: 60
52Lambdaparameter: 106
body: 62
53ExprTuple63, 117
54Operationoperator: 122
operand: 75
55Operationoperator: 90
operands: 65
56Operationoperator: 72
operands: 66
57Operationoperator: 72
operands: 67
58Operationoperator: 68
operands: 69
59Operationoperator: 91
operands: 70
60Operationoperator: 72
operands: 71
61ExprTuple106
62Operationoperator: 72
operands: 73
63Operationoperator: 86
operands: 74
64ExprTuple75
66NamedExprselement: 77
targets: 85
67NamedExprselement: 78
targets: 79
68Literal
69NamedExprsbasis: 80
70NamedExprsoperation: 81
71NamedExprselement: 82
targets: 83
72Literal
73NamedExprselement: 84
targets: 85
74ExprTuple100, 120
75Operationoperator: 86
operands: 87
76Operationoperator: 88
operand: 102
77Operationoperator: 90
operands: 97
78Operationoperator: 91
operands: 92
79Operationoperator: 98
operands: 93
80Literal
81Literal
82Operationoperator: 96
operands: 94
83Operationoperator: 98
operands: 95
84Operationoperator: 96
operands: 97
85Operationoperator: 98
operands: 99
86Literal
87ExprTuple100, 101
88Literal
89ExprTuple102
90Literal
91Literal
92NamedExprsoperation: 103
part: 106
93ExprTuple124, 108
part: 106
95ExprTuple124, 120
96Literal
part: 106
98Literal
99ExprTuple107, 108
100Literal
101Operationoperator: 115
operands: 109
102Literal
103Operationoperator: 110
operands: 111
104Operationoperator: 112
operands: 113
105Literal
106Variable
107Operationoperator: 115
operands: 114
108Operationoperator: 115
operands: 116
109ExprTuple120, 117
110Literal
111ExprTuple118, 120
112Literal
113ExprTuple119, 120
114ExprTuple120, 124
115Literal
116ExprTuple120, 121
117Operationoperator: 122
operand: 124
118Literal
119Variable
120Literal
121Literal
122Literal
123ExprTuple124
124Literal