Expression of type Forall ¶

from the theory of proveit.physics.quantum.QPE ¶

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 ExprRange, U, Variable, VertExprArray, s, t
from proveit.linear_algebra import MatrixMult, ScalarMult, Unitary
from proveit.logic import 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

# 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 = Forall(instance_param_or_params = [s, t], instance_expr = 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(), domain = NaturalPos).with_wrapping()

# 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

# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())

\begin{array}{l}\forall_{s, t \in \mathbb{N}^+}~\\
\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}\right]\end{array}

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

name	description	default	current value	related methods
with_wrapping	If 'True', wrap the Expression after the parameters	None	True	('with_wrapping',)
condition_wrapping	Wrap 'before' or 'after' the condition (or None).	None	None/False	('with_wrap_after_condition', 'with_wrap_before_condition')
wrap_params	If 'True', wraps every two parameters AND wraps the Expression after the parameters	None	None/False	('with_params',)
justification	justify to the 'left', 'center', or 'right' in the array cells	center	center	('with_justification',)

	core type	sub-expressions
0	Operation	operator: 28 operand: 2
1	ExprTuple	2
2	Lambda	parameters: 3 body: 4
3	ExprTuple	163, 171
4	Conditional	value: 5 condition: 6
5	Operation	operator: 28 operand: 9
6	Operation	operator: 43 operands: 8
7	ExprTuple	9
8	ExprTuple	10, 11
9	Lambda	parameter: 160 body: 13
10	Operation	operator: 58 operands: 14
11	Operation	operator: 58 operands: 15
12	ExprTuple	160
13	Conditional	value: 16 condition: 17
14	ExprTuple	163, 18
15	ExprTuple	171, 18
16	Operation	operator: 28 operand: 21
17	Operation	operator: 58 operands: 20
18	Literal
19	ExprTuple	21
20	ExprTuple	160, 22
21	Lambda	parameter: 149 body: 23
22	Operation	operator: 24 operand: 54
23	Conditional	value: 26 condition: 27
24	Literal
25	ExprTuple	54
26	Operation	operator: 28 operand: 31
27	Operation	operator: 43 operands: 30
28	Literal
29	ExprTuple	31
30	ExprTuple	32, 33
31	Lambda	parameter: 167 body: 35
32	Operation	operator: 58 operands: 36
33	Operation	operator: 60 operands: 37
34	ExprTuple	167
35	Conditional	value: 38 condition: 39
36	ExprTuple	149, 40
37	ExprTuple	41, 162
38	Operation	operator: 60 operands: 42
39	Operation	operator: 43 operands: 44
40	Operation	operator: 45 operands: 46
41	Operation	operator: 47 operand: 149
42	ExprTuple	49, 162
43	Literal
44	ExprTuple	50, 51, 52
45	Literal
46	ExprTuple	53, 54
47	Literal
48	ExprTuple	149
49	Operation	operator: 55 operand: 63
50	Operation	operator: 58 operands: 57
51	Operation	operator: 58 operands: 59
52	Operation	operator: 60 operands: 61
53	Literal
54	Operation	operator: 168 operands: 62
55	Literal
56	ExprTuple	63
57	ExprTuple	167, 64
58	Literal
59	ExprTuple	161, 65
60	Literal
61	ExprTuple	66, 67
62	ExprTuple	170, 163
63	Operation	operator: 68 operands: 69
64	Literal
65	Operation	operator: 144 operands: 70
66	Operation	operator: 71 operands: 72
67	Operation	operator: 73 operands: 74
68	Literal
69	ExprTuple	75, 76, 77, 78
70	ExprTuple	79, 80
71	Literal
72	ExprTuple	160, 149
73	Literal
74	ExprTuple	81, 149
75	ExprTuple	82, 83
76	ExprTuple	84, 85
77	ExprTuple	86, 87
78	ExprTuple	88, 89
79	Literal
80	Operation	operator: 158 operands: 90
81	Operation	operator: 168 operands: 91
82	ExprRange	lambda_map: 92 start_index: 162 end_index: 171
83	ExprRange	lambda_map: 93 start_index: 162 end_index: 163
84	ExprRange	lambda_map: 94 start_index: 162 end_index: 171
85	ExprRange	lambda_map: 94 start_index: 151 end_index: 152
86	ExprRange	lambda_map: 95 start_index: 162 end_index: 171
87	ExprRange	lambda_map: 96 start_index: 162 end_index: 163
88	ExprRange	lambda_map: 97 start_index: 162 end_index: 171
89	ExprRange	lambda_map: 98 start_index: 162 end_index: 163
90	ExprTuple	166, 99
91	ExprTuple	100, 101
92	Lambda	parameter: 150 body: 102
93	Lambda	parameter: 150 body: 103
94	Lambda	parameter: 150 body: 104
95	Lambda	parameter: 150 body: 105
96	Lambda	parameter: 150 body: 106
97	Lambda	parameter: 150 body: 107
98	Lambda	parameter: 150 body: 109
99	Operation	operator: 110 operand: 162
100	Literal
101	Operation	operator: 164 operands: 112
102	Operation	operator: 136 operands: 113
103	Operation	operator: 120 operands: 114
104	Operation	operator: 120 operands: 115
105	Operation	operator: 116 operands: 117
106	Operation	operator: 137 operands: 118
107	Operation	operator: 120 operands: 119
108	ExprTuple	150
109	Operation	operator: 120 operands: 121
110	Literal
111	ExprTuple	162
112	ExprTuple	170, 122, 123, 167
113	NamedExprs	state: 124
114	NamedExprs	element: 125 targets: 133
115	NamedExprs	element: 126 targets: 127
116	Literal
117	NamedExprs	basis: 128
118	NamedExprs	operation: 129
119	NamedExprs	element: 130 targets: 131
120	Literal
121	NamedExprs	element: 132 targets: 133
122	Literal
123	Literal
124	Operation	operator: 134 operand: 146
125	Operation	operator: 136 operands: 143
126	Operation	operator: 137 operands: 138
127	Operation	operator: 144 operands: 139
128	Literal
129	Literal
130	Operation	operator: 142 operands: 140
131	Operation	operator: 144 operands: 141
132	Operation	operator: 142 operands: 143
133	Operation	operator: 144 operands: 145
134	Literal
135	ExprTuple	146
136	Literal
137	Literal
138	NamedExprs	operation: 147 part: 150
139	ExprTuple	162, 152
140	NamedExprs	state: 148 part: 150
141	ExprTuple	162, 171
142	Literal
143	NamedExprs	state: 149 part: 150
144	Literal
145	ExprTuple	151, 152
146	Literal
147	Operation	operator: 153 operands: 154
148	Operation	operator: 155 operands: 156
149	Variable
150	Variable
151	Operation	operator: 158 operands: 157
152	Operation	operator: 158 operands: 159
153	Literal
154	ExprTuple	160, 171
155	Literal
156	ExprTuple	161, 171
157	ExprTuple	171, 162
158	Literal
159	ExprTuple	171, 163
160	Variable
161	Operation	operator: 164 operands: 165
162	Literal
163	Variable
164	Literal
165	ExprTuple	166, 167
166	Operation	operator: 168 operands: 169
167	Variable
168	Literal
169	ExprTuple	170, 171
170	Literal
171	Variable

Expression of type Forall¶

from the theory of proveit.physics.quantum.QPE¶

Expression of type Forall ¶

from the theory of proveit.physics.quantum.QPE ¶