Expression of type Lambda

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

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..

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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