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
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_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 = [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()

# 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_{\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}

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