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, NaturalPos, 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(m, Conditional(Forall(instance_param_or_params = [U], instance_expr = 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), domain = Unitary(Exp(two, m))), InSet(m, NaturalPos)))

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

m \mapsto \left\{\forall_{U \in \textrm{U}\left(2^{m}\right)}~\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]\right] \textrm{ if } m \in \mathbb{N}^+\right..

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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