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
from proveit.logic import And, 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_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(var_ket_u, Conditional(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(), And(InSet(var_ket_u, s_ket_domain), normalized_var_ket_u)))

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

\lvert u \rangle \mapsto \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} \textrm{ if } \lvert u \rangle \in \mathbb{C}^{2^{s}} ,  \left \|\lvert u \rangle\right \| = 1\right..

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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