# 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.logic import Equals
from proveit.physics.quantum.QPE import _alpha_m_sqrd, _phase_est_circuit
from proveit.statistics import Prob

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

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

\textrm{Pr}\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|\alpha_{m}\right|^{2}

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