Expression of type Lambda

from the theory of proveit.physics.quantum.QPE

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, Lambda, U, Variable, VertExprArray, s, t
from proveit.linear_algebra import MatrixMult, ScalarMult, Unitary
from proveit.logic import Equals, Forall, InSet
from proveit.numbers import Add, Exp, Interval, IntervalCO, Mod, Mult, Real, Round, e, four, frac, greater, i, one, pi, two, zero
from proveit.physics.quantum import I, NumKet, Z, ket_plus, normalized_var_ket_u, var_ket_u
from proveit.physics.quantum.QPE import QPE, phase, s_ket_domain, two_pow_s, two_pow_t
from proveit.physics.quantum.circuits import Gate, Input, Measure, MultiQubitElem, Output, Qcircuit
from proveit.statistics import Prob

# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = Add(t, one)
sub_expr3 = Add(t, s)
sub_expr4 = Interval(sub_expr2, sub_expr3)
sub_expr5 = MultiQubitElem(element = Gate(operation = QPE(U, t), part = sub_expr1), targets = Interval(one, sub_expr3))
expr = Lambda(U, Conditional(Forall(instance_param_or_params = [var_ket_u], instance_expr = Forall(instance_param_or_params = [phase], instance_expr = greater(Prob(Qcircuit(vert_expr_array = VertExprArray([ExprRange(sub_expr1, Input(state = ket_plus), one, t), ExprRange(sub_expr1, MultiQubitElem(element = Input(state = var_ket_u, part = sub_expr1), targets = sub_expr4), one, s)], [ExprRange(sub_expr1, sub_expr5, one, t), ExprRange(sub_expr1, sub_expr5, sub_expr2, sub_expr3)], [ExprRange(sub_expr1, Measure(basis = Z), one, t), ExprRange(sub_expr1, Gate(operation = I).with_implicit_representation(), one, s)], [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(Mod(Round(Mult(two_pow_t, phase)), two_pow_t), t), part = sub_expr1), targets = Interval(one, t)), one, t), ExprRange(sub_expr1, MultiQubitElem(element = Output(state = var_ket_u, part = sub_expr1), targets = sub_expr4), one, s)]))), frac(four, Exp(pi, two))), domain = Real, conditions = [InSet(phase, IntervalCO(zero, one)), Equals(MatrixMult(U, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, phase)), var_ket_u))]).with_wrapping(), domain = s_ket_domain, condition = normalized_var_ket_u).with_wrapping(), InSet(U, Unitary(two_pow_s))))

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\{\begin{array}{l}\forall_{\lvert u \rangle \in \mathbb{C}^{2^{s}}~|~\left \|\lvert u \rangle\right \| = 1}~\\
\left[\begin{array}{l}\forall_{\varphi \in \mathbb{R}~|~\varphi \in \left[0,1\right), \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} & \multigate{4}{\textrm{QPE}\left(U, t\right)} & \meter & \multiqout{3}{\lvert round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \rangle_{t}} \\
\qin{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} & \ghost{\textrm{QPE}\left(U, t\right)} & \measure{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} \qw & \ghostqout{\lvert round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right) > \frac{4}{\pi^{2}}\right)\end{array}\right]\end{array} \textrm{ if } U \in \textrm{U}\left(2^{s}\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: 149 body: 2
1	ExprTuple	149
2	Conditional	value: 3 condition: 4
3	Operation	operator: 14 operand: 7
4	Operation	operator: 48 operands: 6
5	ExprTuple	7
6	ExprTuple	149, 8
7	Lambda	parameter: 138 body: 9
8	Operation	operator: 10 operand: 42
9	Conditional	value: 12 condition: 13
10	Literal
11	ExprTuple	42
12	Operation	operator: 14 operand: 17
13	Operation	operator: 30 operands: 16
14	Literal
15	ExprTuple	17
16	ExprTuple	18, 19
17	Lambda	parameter: 162 body: 21
18	Operation	operator: 48 operands: 22
19	Operation	operator: 50 operands: 23
20	ExprTuple	162
21	Conditional	value: 24 condition: 25
22	ExprTuple	138, 26
23	ExprTuple	27, 151
24	Operation	operator: 28 operands: 29
25	Operation	operator: 30 operands: 31
26	Operation	operator: 32 operands: 33
27	Operation	operator: 34 operand: 138
28	Literal
29	ExprTuple	36, 37
30	Literal
31	ExprTuple	38, 39, 40
32	Literal
33	ExprTuple	41, 42
34	Literal
35	ExprTuple	138
36	Operation	operator: 43 operands: 44
37	Operation	operator: 45 operand: 55
38	Operation	operator: 48 operands: 47
39	Operation	operator: 48 operands: 49
40	Operation	operator: 50 operands: 51
41	Literal
42	Operation	operator: 163 operands: 52
43	Literal
44	ExprTuple	53, 54
45	Literal
46	ExprTuple	55
47	ExprTuple	162, 56
48	Literal
49	ExprTuple	162, 57
50	Literal
51	ExprTuple	58, 59
52	ExprTuple	165, 152
53	Literal
54	Operation	operator: 163 operands: 60
55	Operation	operator: 61 operands: 62
56	Literal
57	Operation	operator: 63 operands: 64
58	Operation	operator: 65 operands: 66
59	Operation	operator: 67 operands: 68
60	ExprTuple	111, 165
61	Literal
62	ExprTuple	69, 70, 71, 72
63	Literal
64	ExprTuple	73, 151
65	Literal
66	ExprTuple	149, 138
67	Literal
68	ExprTuple	74, 138
69	ExprTuple	75, 76
70	ExprTuple	77, 78
71	ExprTuple	79, 80
72	ExprTuple	81, 82
73	Literal
74	Operation	operator: 163 operands: 83
75	ExprRange	lambda_map: 84 start_index: 151 end_index: 166
76	ExprRange	lambda_map: 85 start_index: 151 end_index: 152
77	ExprRange	lambda_map: 86 start_index: 151 end_index: 166
78	ExprRange	lambda_map: 86 start_index: 140 end_index: 141
79	ExprRange	lambda_map: 87 start_index: 151 end_index: 166
80	ExprRange	lambda_map: 88 start_index: 151 end_index: 152
81	ExprRange	lambda_map: 89 start_index: 151 end_index: 166
82	ExprRange	lambda_map: 90 start_index: 151 end_index: 152
83	ExprTuple	91, 92
84	Lambda	parameter: 139 body: 93
85	Lambda	parameter: 139 body: 94
86	Lambda	parameter: 139 body: 95
87	Lambda	parameter: 139 body: 96
88	Lambda	parameter: 139 body: 97
89	Lambda	parameter: 139 body: 98
90	Lambda	parameter: 139 body: 100
91	Literal
92	Operation	operator: 159 operands: 101
93	Operation	operator: 125 operands: 102
94	Operation	operator: 109 operands: 103
95	Operation	operator: 109 operands: 104
96	Operation	operator: 105 operands: 106
97	Operation	operator: 126 operands: 107
98	Operation	operator: 109 operands: 108
99	ExprTuple	139
100	Operation	operator: 109 operands: 110
101	ExprTuple	165, 111, 112, 162
102	NamedExprs	state: 113
103	NamedExprs	element: 114 targets: 122
104	NamedExprs	element: 115 targets: 116
105	Literal
106	NamedExprs	basis: 117
107	NamedExprs	operation: 118
108	NamedExprs	element: 119 targets: 120
109	Literal
110	NamedExprs	element: 121 targets: 122
111	Literal
112	Literal
113	Operation	operator: 123 operand: 135
114	Operation	operator: 125 operands: 132
115	Operation	operator: 126 operands: 127
116	Operation	operator: 133 operands: 128
117	Literal
118	Literal
119	Operation	operator: 131 operands: 129
120	Operation	operator: 133 operands: 130
121	Operation	operator: 131 operands: 132
122	Operation	operator: 133 operands: 134
123	Literal
124	ExprTuple	135
125	Literal
126	Literal
127	NamedExprs	operation: 136 part: 139
128	ExprTuple	151, 141
129	NamedExprs	state: 137 part: 139
130	ExprTuple	151, 166
131	Literal
132	NamedExprs	state: 138 part: 139
133	Literal
134	ExprTuple	140, 141
135	Literal
136	Operation	operator: 142 operands: 143
137	Operation	operator: 144 operands: 145
138	Variable
139	Variable
140	Operation	operator: 147 operands: 146
141	Operation	operator: 147 operands: 148
142	Literal
143	ExprTuple	149, 166
144	Literal
145	ExprTuple	150, 166
146	ExprTuple	166, 151
147	Literal
148	ExprTuple	166, 152
149	Variable
150	Operation	operator: 153 operands: 154
151	Literal
152	Variable
153	Literal
154	ExprTuple	155, 161
155	Operation	operator: 156 operand: 158
156	Literal
157	ExprTuple	158
158	Operation	operator: 159 operands: 160
159	Literal
160	ExprTuple	161, 162
161	Operation	operator: 163 operands: 164
162	Variable
163	Literal
164	ExprTuple	165, 166
165	Literal
166	Variable