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, eps, m, n, s, t
from proveit.logic import And, InSet
from proveit.numbers import Add, Ceil, Exp, Interval, LessEq, Log, ModAbs, Mult, NaturalPos, Neg, frac, greater_eq, one, subtract, 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 ProbOfAll

# 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(t, Conditional(greater_eq(ProbOfAll(instance_param_or_params = [m], instance_element = 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(m, 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)])), domain = Interval(zero, subtract(two_pow_t, one)), condition = LessEq(ModAbs(subtract(frac(m, two_pow_t), phase), one), Exp(two, Neg(n)))).with_wrapping(), subtract(one, eps)), And(InSet(t, NaturalPos), greater_eq(t, Add(n, Ceil(Log(two, Add(two, frac(one, Mult(two, eps))))))))))

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

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