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, InSet
from proveit.numbers import Add, Exp, Interval, IntervalCO, Mult, NaturalPos, Real, e, i, one, pi, 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 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 = InSet(phase, Real)
sub_expr5 = Interval(sub_expr2, sub_expr3)
sub_expr6 = Mult(two_pow_t, phase)
sub_expr7 = MultiQubitElem(element = Gate(operation = QPE(U, t), part = sub_expr1), targets = Interval(one, sub_expr3))
sub_expr8 = InSet(sub_expr6, Interval(zero, subtract(two_pow_t, one)))
sub_expr9 = Equals(MatrixMult(U, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, phase)), var_ket_u))
sub_expr10 = 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_expr5), one, s)], [ExprRange(sub_expr1, sub_expr7, one, t), ExprRange(sub_expr1, sub_expr7, 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_expr6, 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_expr5), one, s)]))), one)
expr = Conditional(Equals(Conditional(sub_expr10, And(sub_expr4, sub_expr8, sub_expr9, InSet(phase, IntervalCO(zero, one)))), Conditional(sub_expr10, And(sub_expr4, sub_expr8, sub_expr9))), InSet(t, NaturalPos))

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