# 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 Lambda, l, m
from proveit.logic import And, Bijections, InSet
from proveit.numbers import Add, Mod
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 = And(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]\right) \land \left(\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
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',)
In [6]:
# display the expression information
stored_expr.expr_info()

core typesub-expressionsexpression
0Operationoperator: 1
operands: 2
1Literal
2ExprTuple3, 4
3Operationoperator: 6
operands: 5
4Operationoperator: 6
operands: 7
5ExprTuple8, 9
6Literal
7ExprTuple10, 11
8Lambdaparameter: 46
body: 13
9Operationoperator: 17
operands: 14
10Lambdaparameter: 121
body: 16
11Operationoperator: 17
operands: 18
12ExprTuple46
13Operationoperator: 19
operands: 20
14ExprTuple21, 24
15ExprTuple121
16Operationoperator: 22
operands: 23
17Literal
18ExprTuple24, 25
19Literal
20ExprTuple26, 65
21Operationoperator: 100
operands: 27
22Literal
23ExprTuple28, 29, 30, 31
24Operationoperator: 100
operands: 32
25Literal
26Operationoperator: 117
operands: 33
27ExprTuple34, 77
28ExprTuple35, 36
29ExprTuple37, 38
30ExprTuple39, 40
31ExprTuple41, 42
32ExprTuple43, 44
33ExprTuple45, 46
34Operationoperator: 117
operands: 47
35ExprRangelambda_map: 48
start_index: 126
end_index: 122
36ExprRangelambda_map: 49
start_index: 126
end_index: 123
37ExprRangelambda_map: 50
start_index: 126
end_index: 122
38ExprRangelambda_map: 50
start_index: 109
end_index: 110
39ExprRangelambda_map: 51
start_index: 126
end_index: 122
40ExprRangelambda_map: 52
start_index: 126
end_index: 123
41ExprRangelambda_map: 53
start_index: 126
end_index: 122
42ExprRangelambda_map: 54
start_index: 126
end_index: 123
43Literal
44Operationoperator: 117
operands: 55
45Literal
46Variable
47ExprTuple56, 126
48Lambdaparameter: 108
body: 57
49Lambdaparameter: 108
body: 58
50Lambdaparameter: 108
body: 59
51Lambdaparameter: 108
body: 60
52Lambdaparameter: 108
body: 61
53Lambdaparameter: 108
body: 62
54Lambdaparameter: 108
body: 64
55ExprTuple65, 119
56Operationoperator: 124
operand: 77
57Operationoperator: 92
operands: 67
58Operationoperator: 74
operands: 68
59Operationoperator: 74
operands: 69
60Operationoperator: 70
operands: 71
61Operationoperator: 93
operands: 72
62Operationoperator: 74
operands: 73
63ExprTuple108
64Operationoperator: 74
operands: 75
65Operationoperator: 88
operands: 76
66ExprTuple77
68NamedExprselement: 79
targets: 87
69NamedExprselement: 80
targets: 81
70Literal
71NamedExprsbasis: 82
72NamedExprsoperation: 83
73NamedExprselement: 84
targets: 85
74Literal
75NamedExprselement: 86
targets: 87
76ExprTuple102, 122
77Operationoperator: 88
operands: 89
78Operationoperator: 90
operand: 104
79Operationoperator: 92
operands: 99
80Operationoperator: 93
operands: 94
81Operationoperator: 100
operands: 95
82Literal
83Literal
84Operationoperator: 98
operands: 96
85Operationoperator: 100
operands: 97
86Operationoperator: 98
operands: 99
87Operationoperator: 100
operands: 101
88Literal
89ExprTuple102, 103
90Literal
91ExprTuple104
92Literal
93Literal
94NamedExprsoperation: 105
part: 108
95ExprTuple126, 110
part: 108
97ExprTuple126, 122
98Literal
part: 108
100Literal
101ExprTuple109, 110
102Literal
103Operationoperator: 117
operands: 111
104Literal
105Operationoperator: 112
operands: 113
106Operationoperator: 114
operands: 115
107Literal
108Variable
109Operationoperator: 117
operands: 116
110Operationoperator: 117
operands: 118
111ExprTuple122, 119
112Literal
113ExprTuple120, 122
114Literal
115ExprTuple121, 122
116ExprTuple122, 126
117Literal
118ExprTuple122, 123
119Operationoperator: 124
operand: 126
120Literal
121Variable
122Literal
123Literal
124Literal
125ExprTuple126
126Literal