Expression of type Lambda ¶

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 Conditional, ExprRange, IndexedVar, Lambda, U, Variable, m, t
from proveit.linear_algebra import MatrixMult, ScalarMult, Unitary
from proveit.logic import And, Equals, Forall, InSet
from proveit.numbers import Exp, Mult, NaturalPos, 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 = Lambda([m, t], Conditional(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(), And(InSet(m, NaturalPos), InSet(t, NaturalPos))))

# 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())

\left(m, t\right) \mapsto \left\{\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} \textrm{ if } m \in \mathbb{N}^+ ,  t \in \mathbb{N}^+\right..

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

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

Expression of type Lambda¶

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

Expression of type Lambda ¶

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