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