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

# 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}~|~\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}

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