Expression of type Forall

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 ExprRange, U, Variable, VertExprArray, eps, m, n, s, t
from proveit.logic import Forall
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 = Forall(instance_param_or_params = [t], instance_expr = 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)), domain = NaturalPos, condition = greater_eq(t, Add(n, Ceil(Log(two, Add(two, frac(one, Mult(two, eps)))))))).with_wrapping()

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

\begin{array}{l}\forall_{t \in \mathbb{N}^+~|~t \geq \left(n + \left\lceil \textrm{log}_2\left(2 + \frac{1}{2 \cdot \epsilon}\right)\right\rceil\right)}~\\
\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)\right)\end{array}

stored_expr.style_options()

name	description	default	current value	related methods
with_wrapping	If 'True', wrap the Expression after the parameters	None	True	('with_wrapping',)
condition_wrapping	Wrap 'before' or 'after' the condition (or None).	None	None/False	('with_wrap_after_condition', 'with_wrap_before_condition')
wrap_params	If 'True', wraps every two parameters AND wraps the Expression after the parameters	None	None/False	('with_params',)
justification	justify to the 'left', 'center', or 'right' in the array cells	center	center	('with_justification',)

# display the expression information
stored_expr.expr_info()

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