logo

Expression of type Conditional

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 Conditional, e
from proveit.logic import Equals, InSet
from proveit.physics.quantum.QPE import Pfail, _e_domain, _fail_prob_e
In [2]:
# build up the expression from sub-expressions
expr = Conditional(Equals(Pfail(e), _fail_prob_e), InSet(e, _e_domain))
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[P_{\rm fail}\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}} > 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] \textrm{ if } e \in \{1~\ldotp \ldotp~2^{t - 1} - 2\}\right..
In [5]:
stored_expr.style_options()
namedescriptiondefaultcurrent valuerelated methods
condition_delimiter'comma' or 'and'commacomma('with_comma_delimiter', 'with_conjunction_delimiter')
In [6]:
# display the expression information
stored_expr.expr_info()
 core typesub-expressionsexpression
0Conditionalvalue: 1
condition: 2
1Operationoperator: 3
operands: 4
2Operationoperator: 44
operands: 5
3Literal
4ExprTuple6, 7
5ExprTuple57, 8
6Operationoperator: 9
operand: 57
7Operationoperator: 11
operand: 14
8Operationoperator: 104
operands: 13
9Literal
10ExprTuple57
11Literal
12ExprTuple14
13ExprTuple132, 15
14Lambdaparameter: 131
body: 17
15Operationoperator: 126
operands: 18
16ExprTuple131
17Conditionalvalue: 19
condition: 20
18ExprTuple21, 22
19Operationoperator: 23
operands: 24
20Operationoperator: 25
operands: 26
21Operationoperator: 116
operands: 27
22Operationoperator: 119
operand: 128
23Literal
24ExprTuple29, 30, 31, 32
25Literal
26ExprTuple33, 34
27ExprTuple128, 35
28ExprTuple128
29ExprTuple36, 37
30ExprTuple38, 39
31ExprTuple40, 41
32ExprTuple42, 43
33Operationoperator: 44
operands: 45
34Operationoperator: 46
operands: 47
35Operationoperator: 126
operands: 48
36ExprRangelambda_map: 49
start_index: 132
end_index: 133
37ExprRangelambda_map: 50
start_index: 132
end_index: 134
38ExprRangelambda_map: 51
start_index: 132
end_index: 133
39ExprRangelambda_map: 51
start_index: 114
end_index: 115
40ExprRangelambda_map: 52
start_index: 132
end_index: 133
41ExprRangelambda_map: 53
start_index: 132
end_index: 134
42ExprRangelambda_map: 54
start_index: 132
end_index: 133
43ExprRangelambda_map: 55
start_index: 132
end_index: 134
44Literal
45ExprTuple131, 56
46Literal
47ExprTuple57, 58
48ExprTuple133, 107
49Lambdaparameter: 113
body: 59
50Lambdaparameter: 113
body: 60
51Lambdaparameter: 113
body: 61
52Lambdaparameter: 113
body: 62
53Lambdaparameter: 113
body: 63
54Lambdaparameter: 113
body: 64
55Lambdaparameter: 113
body: 66
56Operationoperator: 104
operands: 67
57Variable
58Operationoperator: 68
operands: 69
59Operationoperator: 96
operands: 70
60Operationoperator: 77
operands: 71
61Operationoperator: 77
operands: 72
62Operationoperator: 73
operands: 74
63Operationoperator: 97
operands: 75
64Operationoperator: 77
operands: 76
65ExprTuple113
66Operationoperator: 77
operands: 78
67ExprTuple79, 80
68Literal
69ExprTuple81, 106
70NamedExprsstate: 82
71NamedExprselement: 83
targets: 91
72NamedExprselement: 84
targets: 85
73Literal
74NamedExprsbasis: 86
75NamedExprsoperation: 87
76NamedExprselement: 88
targets: 89
77Literal
78NamedExprselement: 90
targets: 91
79Literal
80Operationoperator: 126
operands: 92
81Operationoperator: 126
operands: 93
82Operationoperator: 94
operand: 109
83Operationoperator: 96
operands: 103
84Operationoperator: 97
operands: 98
85Operationoperator: 104
operands: 99
86Literal
87Literal
88Operationoperator: 102
operands: 100
89Operationoperator: 104
operands: 101
90Operationoperator: 102
operands: 103
91Operationoperator: 104
operands: 105
92ExprTuple106, 107
93ExprTuple131, 108
94Literal
95ExprTuple109
96Literal
97Literal
98NamedExprsoperation: 110
part: 113
99ExprTuple132, 115
100NamedExprsstate: 111
part: 113
101ExprTuple132, 133
102Literal
103NamedExprsstate: 112
part: 113
104Literal
105ExprTuple114, 115
106Operationoperator: 116
operands: 117
107Operationoperator: 119
operand: 132
108Operationoperator: 119
operand: 129
109Literal
110Operationoperator: 121
operands: 122
111Operationoperator: 123
operands: 124
112Literal
113Variable
114Operationoperator: 126
operands: 125
115Operationoperator: 126
operands: 127
116Literal
117ExprTuple128, 133
118ExprTuple132
119Literal
120ExprTuple129
121Literal
122ExprTuple130, 133
123Literal
124ExprTuple131, 133
125ExprTuple133, 132
126Literal
127ExprTuple133, 134
128Literal
129Literal
130Literal
131Variable
132Literal
133Literal
134Literal