Expression of type Conditional

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, 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(varphi, sub_expr1)
sub_expr3 = IndexedVar(U, sub_expr1)
expr = Conditional(Forall(instance_param_or_params = [var_ket_u], instance_expr = 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(sub_expr3, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, sub_expr2)), var_ket_u)), one, t)).with_wrapping(), domain = m_ket_domain, condition = normalized_var_ket_u).with_wrapping(), And(ExprRange(sub_expr1, InSet(sub_expr3, Unitary(Exp(two, m))), one, t)))

expr:

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

name	description	default	current value	related methods
condition_delimiter	'comma' or 'and'	comma	comma	('with_comma_delimiter', 'with_conjunction_delimiter')

# display the expression information
stored_expr.expr_info()

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