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