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