Expression of type Conditional

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, 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, Mult, Real, e, i, one, pi, subtract, 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 = Mult(two_pow_t, phase)
sub_expr6 = MultiQubitElem(element = Gate(operation = QPE(U, t), part = sub_expr1), targets = Interval(one, sub_expr3))
expr = Conditional(Forall(instance_param_or_params = [phase], instance_expr = Equals(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_expr6, one, t), ExprRange(sub_expr1, sub_expr6, 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(sub_expr5, 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)]))), one), domain = Real, conditions = [InSet(sub_expr5, Interval(zero, subtract(two_pow_t, one))), Equals(MatrixMult(U, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, phase)), var_ket_u)), InSet(phase, IntervalCO(zero, one))]), 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())

\left\{\forall_{\varphi \in \mathbb{R}~|~\left(2^{t} \cdot \varphi\right) \in \{0~\ldotp \ldotp~2^{t} - 1\}, \left(U \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi} \cdot \lvert u \rangle\right), \varphi \in \left[0,1\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 2^{t} \cdot \varphi \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert 2^{t} \cdot \varphi \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 2^{t} \cdot \varphi \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert 2^{t} \cdot \varphi \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right) = 1\right) \textrm{ if } \lvert u \rangle \in \mathbb{C}^{2^{s}} ,  \left \|\lvert u \rangle\right \| = 1\right..

stored_expr.style_options()

name	description	default	current value	related methods
condition_delimiter	'comma' or 'and'	comma	comma	('with_comma_delimiter', 'with_conjunction_delimiter')

# display the expression information
stored_expr.expr_info()

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