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, 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, var_ket_u
from proveit.physics.quantum.QPE import QPE, phase, 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(phase, Conditional(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))), And(InSet(phase, Real), InSet(phase, IntervalCO(zero, one)), Equals(MatrixMult(U, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, phase)), 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())

\varphi \mapsto \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}} \textrm{ if } \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)\right..

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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