Expression of type ExprTuple ¶

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, ExprTuple, 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 = ExprTuple(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())

\left(\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..\right)

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

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

Expression of type ExprTuple¶

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

Expression of type ExprTuple ¶

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