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, ExprRange, U, Variable, VertExprArray, s, t
from proveit.linear_algebra import MatrixMult, ScalarMult, Unitary
from proveit.logic import And, Equals, Forall, InSet
from proveit.numbers import Add, Exp, Interval, Mult, NaturalPos, Real, e, i, one, pi, subtract, two, zero
from proveit.physics.quantum import I, NumKet, Z, ket_plus, normalized_var_ket_u, var_ket_u
from proveit.physics.quantum.QPE import QPE, phase, s_ket_domain, two_pow_s, two_pow_t
from proveit.physics.quantum.circuits import Gate, Input, Measure, MultiQubitElem, Output, Qcircuit
from proveit.statistics import Prob
In [2]:
# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = Add(t, one)
sub_expr3 = Add(t, s)
sub_expr4 = Interval(sub_expr2, sub_expr3)
sub_expr5 = Mult(two_pow_t, phase)
sub_expr6 = MultiQubitElem(element = Gate(operation = QPE(U, t), part = sub_expr1), targets = Interval(one, sub_expr3))
expr = Conditional(Forall(instance_param_or_params = [U], instance_expr = Forall(instance_param_or_params = [var_ket_u], instance_expr = Forall(instance_param_or_params = [phase], instance_expr = Equals(Prob(Qcircuit(vert_expr_array = VertExprArray([ExprRange(sub_expr1, Input(state = ket_plus), one, t), ExprRange(sub_expr1, MultiQubitElem(element = Input(state = var_ket_u, part = sub_expr1), targets = sub_expr4), one, s)], [ExprRange(sub_expr1, sub_expr6, one, t), ExprRange(sub_expr1, sub_expr6, sub_expr2, sub_expr3)], [ExprRange(sub_expr1, Measure(basis = Z), one, t), ExprRange(sub_expr1, Gate(operation = I).with_implicit_representation(), one, s)], [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(sub_expr5, t), part = sub_expr1), targets = Interval(one, t)), one, t), ExprRange(sub_expr1, MultiQubitElem(element = Output(state = var_ket_u, part = sub_expr1), targets = sub_expr4), one, s)]))), one), domain = Real, conditions = [InSet(sub_expr5, Interval(zero, subtract(two_pow_t, one))), Equals(MatrixMult(U, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, phase)), var_ket_u))]).with_wrapping(), domain = s_ket_domain, condition = normalized_var_ket_u).with_wrapping(), domain = Unitary(two_pow_s)).with_wrapping(), And(InSet(s, NaturalPos), InSet(t, NaturalPos)))
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\{\begin{array}{l}\forall_{U \in \textrm{U}\left(2^{s}\right)}~\\
\left[\begin{array}{l}\forall_{\lvert u \rangle \in \mathbb{C}^{2^{s}}~|~\left \|\lvert u \rangle\right \| = 1}~\\
\left[\begin{array}{l}\forall_{\varphi \in \mathbb{R}~|~\left(2^{t} \cdot \varphi\right) \in \{0~\ldotp \ldotp~2^{t} - 1\}, \left(U \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi} \cdot \lvert u \rangle\right)}~\\
\left(\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 2^{t} \cdot \varphi \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert 2^{t} \cdot \varphi \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 2^{t} \cdot \varphi \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert 2^{t} \cdot \varphi \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right) = 1\right)\end{array}\right]\end{array}\right]\end{array} \textrm{ if } s \in \mathbb{N}^+ ,  t \in \mathbb{N}^+\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: 24
operand: 5
2Operationoperator: 39
operands: 4
3ExprTuple5
4ExprTuple6, 7
5Lambdaparameter: 156
body: 9
6Operationoperator: 54
operands: 10
7Operationoperator: 54
operands: 11
8ExprTuple156
9Conditionalvalue: 12
condition: 13
10ExprTuple159, 14
11ExprTuple167, 14
12Operationoperator: 24
operand: 17
13Operationoperator: 54
operands: 16
14Literal
15ExprTuple17
16ExprTuple156, 18
17Lambdaparameter: 145
body: 19
18Operationoperator: 20
operand: 50
19Conditionalvalue: 22
condition: 23
20Literal
21ExprTuple50
22Operationoperator: 24
operand: 27
23Operationoperator: 39
operands: 26
24Literal
25ExprTuple27
26ExprTuple28, 29
27Lambdaparameter: 163
body: 31
28Operationoperator: 54
operands: 32
29Operationoperator: 56
operands: 33
30ExprTuple163
31Conditionalvalue: 34
condition: 35
32ExprTuple145, 36
33ExprTuple37, 158
34Operationoperator: 56
operands: 38
35Operationoperator: 39
operands: 40
36Operationoperator: 41
operands: 42
37Operationoperator: 43
operand: 145
38ExprTuple45, 158
39Literal
40ExprTuple46, 47, 48
41Literal
42ExprTuple49, 50
43Literal
44ExprTuple145
45Operationoperator: 51
operand: 59
46Operationoperator: 54
operands: 53
47Operationoperator: 54
operands: 55
48Operationoperator: 56
operands: 57
49Literal
50Operationoperator: 164
operands: 58
51Literal
52ExprTuple59
53ExprTuple163, 60
54Literal
55ExprTuple157, 61
56Literal
57ExprTuple62, 63
58ExprTuple166, 159
59Operationoperator: 64
operands: 65
60Literal
61Operationoperator: 140
operands: 66
62Operationoperator: 67
operands: 68
63Operationoperator: 69
operands: 70
64Literal
65ExprTuple71, 72, 73, 74
66ExprTuple75, 76
67Literal
68ExprTuple156, 145
69Literal
70ExprTuple77, 145
71ExprTuple78, 79
72ExprTuple80, 81
73ExprTuple82, 83
74ExprTuple84, 85
75Literal
76Operationoperator: 154
operands: 86
77Operationoperator: 164
operands: 87
78ExprRangelambda_map: 88
start_index: 158
end_index: 167
79ExprRangelambda_map: 89
start_index: 158
end_index: 159
80ExprRangelambda_map: 90
start_index: 158
end_index: 167
81ExprRangelambda_map: 90
start_index: 147
end_index: 148
82ExprRangelambda_map: 91
start_index: 158
end_index: 167
83ExprRangelambda_map: 92
start_index: 158
end_index: 159
84ExprRangelambda_map: 93
start_index: 158
end_index: 167
85ExprRangelambda_map: 94
start_index: 158
end_index: 159
86ExprTuple162, 95
87ExprTuple96, 97
88Lambdaparameter: 146
body: 98
89Lambdaparameter: 146
body: 99
90Lambdaparameter: 146
body: 100
91Lambdaparameter: 146
body: 101
92Lambdaparameter: 146
body: 102
93Lambdaparameter: 146
body: 103
94Lambdaparameter: 146
body: 105
95Operationoperator: 106
operand: 158
96Literal
97Operationoperator: 160
operands: 108
98Operationoperator: 132
operands: 109
99Operationoperator: 116
operands: 110
100Operationoperator: 116
operands: 111
101Operationoperator: 112
operands: 113
102Operationoperator: 133
operands: 114
103Operationoperator: 116
operands: 115
104ExprTuple146
105Operationoperator: 116
operands: 117
106Literal
107ExprTuple158
108ExprTuple166, 118, 119, 163
109NamedExprsstate: 120
110NamedExprselement: 121
targets: 129
111NamedExprselement: 122
targets: 123
112Literal
113NamedExprsbasis: 124
114NamedExprsoperation: 125
115NamedExprselement: 126
targets: 127
116Literal
117NamedExprselement: 128
targets: 129
118Literal
119Literal
120Operationoperator: 130
operand: 142
121Operationoperator: 132
operands: 139
122Operationoperator: 133
operands: 134
123Operationoperator: 140
operands: 135
124Literal
125Literal
126Operationoperator: 138
operands: 136
127Operationoperator: 140
operands: 137
128Operationoperator: 138
operands: 139
129Operationoperator: 140
operands: 141
130Literal
131ExprTuple142
132Literal
133Literal
134NamedExprsoperation: 143
part: 146
135ExprTuple158, 148
136NamedExprsstate: 144
part: 146
137ExprTuple158, 167
138Literal
139NamedExprsstate: 145
part: 146
140Literal
141ExprTuple147, 148
142Literal
143Operationoperator: 149
operands: 150
144Operationoperator: 151
operands: 152
145Variable
146Variable
147Operationoperator: 154
operands: 153
148Operationoperator: 154
operands: 155
149Literal
150ExprTuple156, 167
151Literal
152ExprTuple157, 167
153ExprTuple167, 158
154Literal
155ExprTuple167, 159
156Variable
157Operationoperator: 160
operands: 161
158Literal
159Variable
160Literal
161ExprTuple162, 163
162Operationoperator: 164
operands: 165
163Variable
164Literal
165ExprTuple166, 167
166Literal
167Variable