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

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

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