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
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}")
expr = 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, IndexedVar(varphi, sub_expr1))), var_ket_u)), 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\{\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()

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