Expression of type Forall ¶

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

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, IndexedVar, U, Variable, m, t
from proveit.linear_algebra import MatrixMult, ScalarMult, Unitary
from proveit.logic import Equals, Forall
from proveit.numbers import Exp, Mult, e, i, one, pi, two
from proveit.physics.quantum import m_ket_domain, normalized_var_ket_u, var_ket_u, varphi
from proveit.physics.quantum.circuits import phase_kickback_on_register_circuit
from proveit.statistics import Prob

# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = IndexedVar(U, sub_expr1)
sub_expr3 = IndexedVar(varphi, sub_expr1)
expr = Forall(instance_param_or_params = [ExprRange(sub_expr1, sub_expr2, one, t)], instance_expr = Forall(instance_param_or_params = [var_ket_u], instance_expr = Forall(instance_param_or_params = [ExprRange(sub_expr1, sub_expr3, one, t)], instance_expr = Equals(Prob(phase_kickback_on_register_circuit), one), condition = ExprRange(sub_expr1, Equals(MatrixMult(sub_expr2, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, sub_expr3)), var_ket_u)), one, t)).with_wrapping(), domain = m_ket_domain, condition = normalized_var_ket_u).with_wrapping(), domain = Unitary(Exp(two, m))).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_{1}, U_{2}, \ldots, U_{t} \in \textrm{U}\left(2^{m}\right)}~\\
\left[\begin{array}{l}\forall_{\lvert u \rangle \in \mathbb{C}^{2^{m}}~|~\left \|\lvert u \rangle\right \| = 1}~\\
\left[\begin{array}{l}\forall_{\varphi_{1}, \varphi_{2}, \ldots, \varphi_{t}~|~\left(\left(U_{1} \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{1}} \cdot \lvert u \rangle\right)\right), \left(\left(U_{2} \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{2}} \cdot \lvert u \rangle\right)\right), \ldots, \left(\left(U_{t} \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{t}} \cdot \lvert u \rangle\right)\right)}~\\
\left(\textrm{Pr}\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \control{} \qw \qwx[1] & \qw & \gate{\cdots} \qwx[1] & \qw & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{1}} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\lvert + \rangle} & \qw \qwx[1] & \control{} \qw \qwx[1] & \gate{\cdots} \qwx[1] & \qw & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{2}} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} & \gate{\vdots} \qwx[1] & \gate{\vdots} \qwx[1] & \gate{\ddots} \qwx[1] & \gate{\vdots} & \qout{\vdots} \\
\qin{\lvert + \rangle} & \qw \qwx[1] & \qw \qwx[1] & \gate{\cdots} \qwx[1] & \control{} \qw \qwx[1] & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{t}} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\lvert u \rangle} & \gate{U_{1}} & \gate{U_{2}} & \gate{\cdots} & \gate{U_{t}} & \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: 18 operand: 2
1	ExprTuple	2
2	Lambda	parameters: 3 body: 4
3	ExprTuple	5
4	Conditional	value: 6 condition: 7
5	ExprRange	lambda_map: 8 start_index: 164 end_index: 163
6	Operation	operator: 18 operand: 11
7	Operation	operator: 40 operands: 10
8	Lambda	parameter: 173 body: 77
9	ExprTuple	11
10	ExprTuple	12
11	Lambda	parameter: 111 body: 13
12	ExprRange	lambda_map: 14 start_index: 164 end_index: 163
13	Conditional	value: 15 condition: 16
14	Lambda	parameter: 173 body: 17
15	Operation	operator: 18 operand: 22
16	Operation	operator: 40 operands: 20
17	Operation	operator: 28 operands: 21
18	Literal
19	ExprTuple	22
20	ExprTuple	23, 24
21	ExprTuple	77, 25
22	Lambda	parameters: 26 body: 27
23	Operation	operator: 28 operands: 29
24	Operation	operator: 124 operands: 30
25	Operation	operator: 31 operand: 49
26	ExprTuple	33
27	Conditional	value: 34 condition: 35
28	Literal
29	ExprTuple	111, 36
30	ExprTuple	37, 164
31	Literal
32	ExprTuple	49
33	ExprRange	lambda_map: 38 start_index: 164 end_index: 163
34	Operation	operator: 124 operands: 39
35	Operation	operator: 40 operands: 41
36	Operation	operator: 42 operands: 43
37	Operation	operator: 44 operand: 111
38	Lambda	parameter: 173 body: 170
39	ExprTuple	46, 164
40	Literal
41	ExprTuple	47
42	Literal
43	ExprTuple	48, 49
44	Literal
45	ExprTuple	111
46	Operation	operator: 50 operand: 54
47	ExprRange	lambda_map: 52 start_index: 164 end_index: 163
48	Literal
49	Operation	operator: 155 operands: 53
50	Literal
51	ExprTuple	54
52	Lambda	parameter: 173 body: 55
53	ExprTuple	167, 147
54	Operation	operator: 56 operands: 57
55	Operation	operator: 124 operands: 58
56	Literal
57	ExprTuple	59, 60, 61
58	ExprTuple	62, 63
59	ExprTuple	64, 65
60	ExprRange	lambda_map: 66 start_index: 164 end_index: 163
61	ExprTuple	67, 68
62	Operation	operator: 69 operands: 70
63	Operation	operator: 142 operands: 71
64	ExprRange	lambda_map: 72 start_index: 164 end_index: 163
65	ExprRange	lambda_map: 73 start_index: 164 end_index: 147
66	Lambda	parameter: 146 body: 74
67	ExprRange	lambda_map: 75 start_index: 164 end_index: 163
68	ExprRange	lambda_map: 76 start_index: 164 end_index: 147
69	Literal
70	ExprTuple	77, 111
71	ExprTuple	150, 111
72	Lambda	parameter: 173 body: 78
73	Lambda	parameter: 173 body: 79
74	ExprTuple	80, 81
75	Lambda	parameter: 173 body: 82
76	Lambda	parameter: 173 body: 83
77	IndexedVar	variable: 137 index: 173
78	Operation	operator: 97 operands: 84
79	Operation	operator: 122 operands: 85
80	ExprRange	lambda_map: 86 start_index: 164 end_index: 163
81	ExprRange	lambda_map: 87 start_index: 164 end_index: 147
82	Operation	operator: 102 operands: 88
83	Operation	operator: 122 operands: 89
84	NamedExprs	state: 90
85	NamedExprs	element: 91 targets: 108
86	Lambda	parameter: 173 body: 92
87	Lambda	parameter: 173 body: 93
88	NamedExprs	state: 94
89	NamedExprs	element: 95 targets: 108
90	Operation	operator: 157 operand: 104
91	Operation	operator: 97 operands: 103
92	Operation	operator: 98 operands: 99
93	Operation	operator: 122 operands: 100
94	Operation	operator: 142 operands: 101
95	Operation	operator: 102 operands: 103
96	ExprTuple	104
97	Literal
98	Literal
99	ExprTuple	105, 106
100	NamedExprs	element: 107 targets: 108
101	ExprTuple	109, 110
102	Literal
103	NamedExprs	state: 111 part: 173
104	Literal
105	Conditional	value: 112 condition: 113
106	Conditional	value: 114 condition: 115
107	Operation	operator: 125 operands: 116
108	Operation	operator: 117 operands: 118
109	Operation	operator: 153 operands: 119
110	Operation	operator: 120 operands: 121
111	Variable
112	Operation	operator: 122 operands: 123
113	Operation	operator: 124 operands: 128
114	Operation	operator: 125 operands: 126
115	Operation	operator: 127 operands: 128
116	NamedExprs	operation: 129 part: 173
117	Literal
118	ExprTuple	152, 130
119	ExprTuple	164, 131
120	Literal
121	ExprTuple	132, 133
122	Literal
123	NamedExprs	element: 134 targets: 135
124	Literal
125	Literal
126	NamedExprs	operation: 136
127	Literal
128	ExprTuple	146, 173
129	IndexedVar	variable: 137 index: 146
130	Operation	operator: 159 operands: 139
131	Operation	operator: 155 operands: 140
132	Operation	operator: 157 operand: 149
133	Operation	operator: 142 operands: 143
134	Literal
135	Operation	operator: 144 operand: 152
136	Literal
137	Variable
138	ExprTuple	146
139	ExprTuple	163, 147
140	ExprTuple	167, 148
141	ExprTuple	149
142	Literal
143	ExprTuple	150, 151
144	Literal
145	ExprTuple	152
146	Variable
147	Variable
148	Operation	operator: 153 operands: 154
149	Literal
150	Operation	operator: 155 operands: 156
151	Operation	operator: 157 operand: 164
152	Operation	operator: 159 operands: 160
153	Literal
154	ExprTuple	164, 167
155	Literal
156	ExprTuple	161, 162
157	Literal
158	ExprTuple	164
159	Literal
160	ExprTuple	163, 164
161	Literal
162	Operation	operator: 165 operands: 166
163	Variable
164	Literal
165	Literal
166	ExprTuple	167, 168, 169, 170
167	Literal
168	Literal
169	Literal
170	IndexedVar	variable: 171 index: 173
171	Variable
172	ExprTuple	173
173	Variable

Expression of type Forall¶

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

Expression of type Forall ¶

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