logo

Expression of type ExprTuple

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, ExprTuple, Lambda, m
from proveit.logic import And, InSet
from proveit.physics.quantum.QPE import _m_domain, _phase_est_circuit, _success_cond
In [2]:
# build up the expression from sub-expressions
expr = ExprTuple(Lambda(m, Conditional(_phase_est_circuit, And(InSet(m, _m_domain), _success_cond))))
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(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} \textrm{ if } m \in \{0~\ldotp \ldotp~2^{t} - 1\} ,  \left|\frac{m}{2^{t}} - \varphi\right|_{\textup{mod}\thinspace 1} \leq 2^{-n}\right..\right)
In [5]:
stored_expr.style_options()
no style options
In [6]:
# display the expression information
stored_expr.expr_info()
 core typesub-expressionsexpression
0ExprTuple1
1Lambdaparameter: 114
body: 3
2ExprTuple114
3Conditionalvalue: 4
condition: 5
4Operationoperator: 6
operands: 7
5Operationoperator: 8
operands: 9
6Literal
7ExprTuple10, 11, 12, 13
8Literal
9ExprTuple14, 15
10ExprTuple16, 17
11ExprTuple18, 19
12ExprTuple20, 21
13ExprTuple22, 23
14Operationoperator: 24
operands: 25
15Operationoperator: 26
operands: 27
16ExprRangelambda_map: 28
start_index: 115
end_index: 120
17ExprRangelambda_map: 29
start_index: 115
end_index: 116
18ExprRangelambda_map: 30
start_index: 115
end_index: 120
19ExprRangelambda_map: 30
start_index: 97
end_index: 98
20ExprRangelambda_map: 31
start_index: 115
end_index: 120
21ExprRangelambda_map: 32
start_index: 115
end_index: 116
22ExprRangelambda_map: 33
start_index: 115
end_index: 120
23ExprRangelambda_map: 34
start_index: 115
end_index: 116
24Literal
25ExprTuple114, 35
26Literal
27ExprTuple36, 37
28Lambdaparameter: 96
body: 38
29Lambdaparameter: 96
body: 39
30Lambdaparameter: 96
body: 40
31Lambdaparameter: 96
body: 41
32Lambdaparameter: 96
body: 42
33Lambdaparameter: 96
body: 43
34Lambdaparameter: 96
body: 45
35Operationoperator: 86
operands: 46
36Operationoperator: 47
operands: 48
37Operationoperator: 117
operands: 49
38Operationoperator: 78
operands: 50
39Operationoperator: 57
operands: 51
40Operationoperator: 57
operands: 52
41Operationoperator: 53
operands: 54
42Operationoperator: 79
operands: 55
43Operationoperator: 57
operands: 56
44ExprTuple96
45Operationoperator: 57
operands: 58
46ExprTuple59, 60
47Literal
48ExprTuple61, 115
49ExprTuple119, 62
50NamedExprsstate: 63
51NamedExprselement: 64
targets: 72
52NamedExprselement: 65
targets: 66
53Literal
54NamedExprsbasis: 67
55NamedExprsoperation: 68
56NamedExprselement: 69
targets: 70
57Literal
58NamedExprselement: 71
targets: 72
59Literal
60Operationoperator: 109
operands: 73
61Operationoperator: 109
operands: 74
62Operationoperator: 102
operand: 91
63Operationoperator: 76
operand: 92
64Operationoperator: 78
operands: 85
65Operationoperator: 79
operands: 80
66Operationoperator: 86
operands: 81
67Literal
68Literal
69Operationoperator: 84
operands: 82
70Operationoperator: 86
operands: 83
71Operationoperator: 84
operands: 85
72Operationoperator: 86
operands: 87
73ExprTuple111, 88
74ExprTuple89, 90
75ExprTuple91
76Literal
77ExprTuple92
78Literal
79Literal
80NamedExprsoperation: 93
part: 96
81ExprTuple115, 98
82NamedExprsstate: 94
part: 96
83ExprTuple115, 120
84Literal
85NamedExprsstate: 95
part: 96
86Literal
87ExprTuple97, 98
88Operationoperator: 102
operand: 115
89Operationoperator: 100
operands: 101
90Operationoperator: 102
operand: 112
91Literal
92Literal
93Operationoperator: 104
operands: 105
94Operationoperator: 106
operands: 107
95Literal
96Variable
97Operationoperator: 109
operands: 108
98Operationoperator: 109
operands: 110
99ExprTuple115
100Literal
101ExprTuple114, 111
102Literal
103ExprTuple112
104Literal
105ExprTuple113, 120
106Literal
107ExprTuple114, 120
108ExprTuple120, 115
109Literal
110ExprTuple120, 116
111Operationoperator: 117
operands: 118
112Literal
113Literal
114Variable
115Literal
116Literal
117Literal
118ExprTuple119, 120
119Literal
120Literal