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, IntervalCO, Mod, Mult, Real, Round, e, four, frac, greater, i, one, pi, 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 = MultiQubitElem(element = Gate(operation = QPE(U, t), part = sub_expr1), targets = Interval(one, sub_expr3))
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 = greater(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_expr5, one, t), ExprRange(sub_expr1, sub_expr5, 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(Mod(Round(Mult(two_pow_t, phase)), two_pow_t), 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)]))), frac(four, Exp(pi, two))), domain = Real, conditions = [InSet(phase, IntervalCO(zero, 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()

# 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_{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}~|~\varphi \in \left[0,1\right), \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 round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \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 round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right) > \frac{4}{\pi^{2}}\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: 16 operand: 2
1	ExprTuple	2
2	Lambda	parameter: 151 body: 4
3	ExprTuple	151
4	Conditional	value: 5 condition: 6
5	Operation	operator: 16 operand: 9
6	Operation	operator: 50 operands: 8
7	ExprTuple	9
8	ExprTuple	151, 10
9	Lambda	parameter: 140 body: 11
10	Operation	operator: 12 operand: 44
11	Conditional	value: 14 condition: 15
12	Literal
13	ExprTuple	44
14	Operation	operator: 16 operand: 19
15	Operation	operator: 32 operands: 18
16	Literal
17	ExprTuple	19
18	ExprTuple	20, 21
19	Lambda	parameter: 164 body: 23
20	Operation	operator: 50 operands: 24
21	Operation	operator: 52 operands: 25
22	ExprTuple	164
23	Conditional	value: 26 condition: 27
24	ExprTuple	140, 28
25	ExprTuple	29, 153
26	Operation	operator: 30 operands: 31
27	Operation	operator: 32 operands: 33
28	Operation	operator: 34 operands: 35
29	Operation	operator: 36 operand: 140
30	Literal
31	ExprTuple	38, 39
32	Literal
33	ExprTuple	40, 41, 42
34	Literal
35	ExprTuple	43, 44
36	Literal
37	ExprTuple	140
38	Operation	operator: 45 operands: 46
39	Operation	operator: 47 operand: 57
40	Operation	operator: 50 operands: 49
41	Operation	operator: 50 operands: 51
42	Operation	operator: 52 operands: 53
43	Literal
44	Operation	operator: 165 operands: 54
45	Literal
46	ExprTuple	55, 56
47	Literal
48	ExprTuple	57
49	ExprTuple	164, 58
50	Literal
51	ExprTuple	164, 59
52	Literal
53	ExprTuple	60, 61
54	ExprTuple	167, 154
55	Literal
56	Operation	operator: 165 operands: 62
57	Operation	operator: 63 operands: 64
58	Literal
59	Operation	operator: 65 operands: 66
60	Operation	operator: 67 operands: 68
61	Operation	operator: 69 operands: 70
62	ExprTuple	113, 167
63	Literal
64	ExprTuple	71, 72, 73, 74
65	Literal
66	ExprTuple	75, 153
67	Literal
68	ExprTuple	151, 140
69	Literal
70	ExprTuple	76, 140
71	ExprTuple	77, 78
72	ExprTuple	79, 80
73	ExprTuple	81, 82
74	ExprTuple	83, 84
75	Literal
76	Operation	operator: 165 operands: 85
77	ExprRange	lambda_map: 86 start_index: 153 end_index: 168
78	ExprRange	lambda_map: 87 start_index: 153 end_index: 154
79	ExprRange	lambda_map: 88 start_index: 153 end_index: 168
80	ExprRange	lambda_map: 88 start_index: 142 end_index: 143
81	ExprRange	lambda_map: 89 start_index: 153 end_index: 168
82	ExprRange	lambda_map: 90 start_index: 153 end_index: 154
83	ExprRange	lambda_map: 91 start_index: 153 end_index: 168
84	ExprRange	lambda_map: 92 start_index: 153 end_index: 154
85	ExprTuple	93, 94
86	Lambda	parameter: 141 body: 95
87	Lambda	parameter: 141 body: 96
88	Lambda	parameter: 141 body: 97
89	Lambda	parameter: 141 body: 98
90	Lambda	parameter: 141 body: 99
91	Lambda	parameter: 141 body: 100
92	Lambda	parameter: 141 body: 102
93	Literal
94	Operation	operator: 161 operands: 103
95	Operation	operator: 127 operands: 104
96	Operation	operator: 111 operands: 105
97	Operation	operator: 111 operands: 106
98	Operation	operator: 107 operands: 108
99	Operation	operator: 128 operands: 109
100	Operation	operator: 111 operands: 110
101	ExprTuple	141
102	Operation	operator: 111 operands: 112
103	ExprTuple	167, 113, 114, 164
104	NamedExprs	state: 115
105	NamedExprs	element: 116 targets: 124
106	NamedExprs	element: 117 targets: 118
107	Literal
108	NamedExprs	basis: 119
109	NamedExprs	operation: 120
110	NamedExprs	element: 121 targets: 122
111	Literal
112	NamedExprs	element: 123 targets: 124
113	Literal
114	Literal
115	Operation	operator: 125 operand: 137
116	Operation	operator: 127 operands: 134
117	Operation	operator: 128 operands: 129
118	Operation	operator: 135 operands: 130
119	Literal
120	Literal
121	Operation	operator: 133 operands: 131
122	Operation	operator: 135 operands: 132
123	Operation	operator: 133 operands: 134
124	Operation	operator: 135 operands: 136
125	Literal
126	ExprTuple	137
127	Literal
128	Literal
129	NamedExprs	operation: 138 part: 141
130	ExprTuple	153, 143
131	NamedExprs	state: 139 part: 141
132	ExprTuple	153, 168
133	Literal
134	NamedExprs	state: 140 part: 141
135	Literal
136	ExprTuple	142, 143
137	Literal
138	Operation	operator: 144 operands: 145
139	Operation	operator: 146 operands: 147
140	Variable
141	Variable
142	Operation	operator: 149 operands: 148
143	Operation	operator: 149 operands: 150
144	Literal
145	ExprTuple	151, 168
146	Literal
147	ExprTuple	152, 168
148	ExprTuple	168, 153
149	Literal
150	ExprTuple	168, 154
151	Variable
152	Operation	operator: 155 operands: 156
153	Literal
154	Variable
155	Literal
156	ExprTuple	157, 163
157	Operation	operator: 158 operand: 160
158	Literal
159	ExprTuple	160
160	Operation	operator: 161 operands: 162
161	Literal
162	ExprTuple	163, 164
163	Operation	operator: 165 operands: 166
164	Variable
165	Literal
166	ExprTuple	167, 168
167	Literal
168	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 ¶