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
from proveit.numbers import Exp, Mult, e, i, one, pi, two
from proveit.physics.quantum import 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([ExprRange(sub_expr1, sub_expr2, one, t)], Conditional(Equals(Prob(phase_kickback_on_register_circuit), one), And(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))))

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