Expression of type ExprTuple

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, ExprTuple, 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 = ExprTuple(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())

\left(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..\right)

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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