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, ExprTuple, Lambda, U, m
from proveit.linear_algebra import ScalarMult, Unitary
from proveit.logic import Equals, Forall, InSet
from proveit.numbers import Exp, Mult, e, i, one, pi, two
from proveit.physics.quantum import Qmult, m_ket_domain, normalized_var_ket_u, var_ket_u, varphi
from proveit.physics.quantum.circuits import phase_kickback_circuit
from proveit.statistics import Prob

# build up the expression from sub-expressions
expr = ExprTuple(Lambda(U, Conditional(Forall(instance_param_or_params = [var_ket_u], instance_expr = Forall(instance_param_or_params = [varphi], instance_expr = Equals(Prob(phase_kickback_circuit), one), condition = Equals(Qmult(U, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, varphi)), var_ket_u))), domain = m_ket_domain, condition = normalized_var_ket_u), InSet(U, Unitary(Exp(two, m))))))

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(U \mapsto \left\{\forall_{\lvert u \rangle \in \mathbb{C}^{2^{m}}~|~\left \|\lvert u \rangle\right \| = 1}~\left[\forall_{\varphi~|~\left(U \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi} \cdot \lvert u \rangle\right)}~\left(\textrm{Pr}\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \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} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\lvert u \rangle} & \gate{U} & \qout{\lvert u \rangle}
} \end{array}\right) = 1\right)\right] \textrm{ if } U \in \textrm{U}\left(2^{m}\right)\right..\right)

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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