logo

Axiom _success_def of type Forall

from the theory of proveit.physics.quantum.QPE

see dependencies

In [1]:
import proveit
# Automation is not needed when only building an expression:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%load_axiom_expr # Load the stored axiom expression as 'stored_expr'
# import the special expression
from proveit.physics.quantum.QPE import _success_def
In [2]:
# check that the built expression is the same as the stored expression
assert _success_def.expr == stored_expr
assert _success_def.expr._style_id == stored_expr._style_id
print("Passed sanity check: _success_def matches stored_expr")
Passed sanity check: _success_def matches stored_expr
In [3]:
# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())
\begin{array}{l}\forall_{e \in \{1~\ldotp \ldotp~2^{t - 1} - 2\}}~\\
\left(\left[P_{\rm success}\right]\left(e\right) = \left[\begin{array}{l}\textrm{Prob}_{m \in \{0~\ldotp \ldotp~2^{t} - 1\}~|~\left|m - b_{\textit{f}}\right|_{\textup{mod}\thinspace 2^{t}} \leq e}~\\
\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)\end{array}\right]\right)\end{array}
In [4]:
stored_expr.style_options()
namedescriptiondefaultcurrent valuerelated methods
with_wrappingIf 'True', wrap the Expression after the parametersNoneTrue('with_wrapping',)
condition_wrappingWrap 'before' or 'after' the condition (or None).NoneNone/False('with_wrap_after_condition', 'with_wrap_before_condition')
wrap_paramsIf 'True', wraps every two parameters AND wraps the Expression after the parametersNoneNone/False('with_params',)
justificationjustify to the 'left', 'center', or 'right' in the array cellscentercenter('with_justification',)
In [5]:
# display the expression information
stored_expr.expr_info()
 core typesub-expressionsexpression
0Operationoperator: 1
operand: 3
1Literal
2ExprTuple3
3Lambdaparameter: 62
body: 4
4Conditionalvalue: 5
condition: 6
5Operationoperator: 7
operands: 8
6Operationoperator: 48
operands: 9
7Literal
8ExprTuple10, 11
9ExprTuple62, 12
10Operationoperator: 13
operand: 62
11Operationoperator: 15
operand: 18
12Operationoperator: 108
operands: 17
13Literal
14ExprTuple62
15Literal
16ExprTuple18
17ExprTuple136, 19
18Lambdaparameter: 135
body: 21
19Operationoperator: 130
operands: 22
20ExprTuple135
21Conditionalvalue: 23
condition: 24
22ExprTuple25, 26
23Operationoperator: 27
operands: 28
24Operationoperator: 29
operands: 30
25Operationoperator: 120
operands: 31
26Operationoperator: 123
operand: 132
27Literal
28ExprTuple33, 34, 35, 36
29Literal
30ExprTuple37, 38
31ExprTuple132, 39
32ExprTuple132
33ExprTuple40, 41
34ExprTuple42, 43
35ExprTuple44, 45
36ExprTuple46, 47
37Operationoperator: 48
operands: 49
38Operationoperator: 50
operands: 51
39Operationoperator: 130
operands: 52
40ExprRangelambda_map: 53
start_index: 136
end_index: 137
41ExprRangelambda_map: 54
start_index: 136
end_index: 138
42ExprRangelambda_map: 55
start_index: 136
end_index: 137
43ExprRangelambda_map: 55
start_index: 118
end_index: 119
44ExprRangelambda_map: 56
start_index: 136
end_index: 137
45ExprRangelambda_map: 57
start_index: 136
end_index: 138
46ExprRangelambda_map: 58
start_index: 136
end_index: 137
47ExprRangelambda_map: 59
start_index: 136
end_index: 138
48Literal
49ExprTuple135, 60
50Literal
51ExprTuple61, 62
52ExprTuple137, 111
53Lambdaparameter: 117
body: 63
54Lambdaparameter: 117
body: 64
55Lambdaparameter: 117
body: 65
56Lambdaparameter: 117
body: 66
57Lambdaparameter: 117
body: 67
58Lambdaparameter: 117
body: 68
59Lambdaparameter: 117
body: 70
60Operationoperator: 108
operands: 71
61Operationoperator: 72
operands: 73
62Variable
63Operationoperator: 100
operands: 74
64Operationoperator: 81
operands: 75
65Operationoperator: 81
operands: 76
66Operationoperator: 77
operands: 78
67Operationoperator: 101
operands: 79
68Operationoperator: 81
operands: 80
69ExprTuple117
70Operationoperator: 81
operands: 82
71ExprTuple83, 84
72Literal
73ExprTuple85, 110
74NamedExprsstate: 86
75NamedExprselement: 87
targets: 95
76NamedExprselement: 88
targets: 89
77Literal
78NamedExprsbasis: 90
79NamedExprsoperation: 91
80NamedExprselement: 92
targets: 93
81Literal
82NamedExprselement: 94
targets: 95
83Literal
84Operationoperator: 130
operands: 96
85Operationoperator: 130
operands: 97
86Operationoperator: 98
operand: 113
87Operationoperator: 100
operands: 107
88Operationoperator: 101
operands: 102
89Operationoperator: 108
operands: 103
90Literal
91Literal
92Operationoperator: 106
operands: 104
93Operationoperator: 108
operands: 105
94Operationoperator: 106
operands: 107
95Operationoperator: 108
operands: 109
96ExprTuple110, 111
97ExprTuple135, 112
98Literal
99ExprTuple113
100Literal
101Literal
102NamedExprsoperation: 114
part: 117
103ExprTuple136, 119
104NamedExprsstate: 115
part: 117
105ExprTuple136, 137
106Literal
107NamedExprsstate: 116
part: 117
108Literal
109ExprTuple118, 119
110Operationoperator: 120
operands: 121
111Operationoperator: 123
operand: 136
112Operationoperator: 123
operand: 133
113Literal
114Operationoperator: 125
operands: 126
115Operationoperator: 127
operands: 128
116Literal
117Variable
118Operationoperator: 130
operands: 129
119Operationoperator: 130
operands: 131
120Literal
121ExprTuple132, 137
122ExprTuple136
123Literal
124ExprTuple133
125Literal
126ExprTuple134, 137
127Literal
128ExprTuple135, 137
129ExprTuple137, 136
130Literal
131ExprTuple137, 138
132Literal
133Literal
134Literal
135Variable
136Literal
137Literal
138Literal