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, 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([ExprRange(sub_expr1, sub_expr2, one, t)], Conditional(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(), And(ExprRange(sub_expr1, InSet(sub_expr2, Unitary(Exp(two, m))), one, t))))

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