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