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, t
from proveit.linear_algebra import MatrixMult, ScalarMult
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(varphi, sub_expr1)
expr = Lambda(var_ket_u, Conditional(Forall(instance_param_or_params = [ExprRange(sub_expr1, sub_expr2, one, t)], instance_expr = Equals(Prob(phase_kickback_on_register_circuit), one), condition = ExprRange(sub_expr1, Equals(MatrixMult(IndexedVar(U, sub_expr1), var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, sub_expr2)), var_ket_u)), one, t)).with_wrapping(), And(InSet(var_ket_u, m_ket_domain), normalized_var_ket_u)))

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

\lvert u \rangle \mapsto \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} \textrm{ if } \lvert u \rangle \in \mathbb{C}^{2^{m}} ,  \left \|\lvert u \rangle\right \| = 1\right..

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

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