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, Forall, 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 = [s, t, U, var_ket_u, phase]
sub_expr3 = Add(t, one)
sub_expr4 = Add(t, s)
sub_expr5 = InSet(phase, Real)
sub_expr6 = InSet(t, NaturalPos)
sub_expr7 = Interval(sub_expr3, sub_expr4)
sub_expr8 = Mult(two_pow_t, phase)
sub_expr9 = MultiQubitElem(element = Gate(operation = QPE(U, t), part = sub_expr1), targets = Interval(one, sub_expr4))
sub_expr10 = InSet(sub_expr8, Interval(zero, subtract(two_pow_t, one)))
sub_expr11 = Equals(MatrixMult(U, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, phase)), var_ket_u))
sub_expr12 = 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_expr7), one, s)], [ExprRange(sub_expr1, sub_expr9, one, t), ExprRange(sub_expr1, sub_expr9, sub_expr3, sub_expr4)], [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_expr8, 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_expr7), one, s)]))), one)
sub_expr13 = Conditional(sub_expr12, And(sub_expr5, sub_expr10, sub_expr11, InSet(phase, IntervalCO(zero, one))))
sub_expr14 = Conditional(sub_expr12, And(sub_expr5, sub_expr10, sub_expr11))
expr = ExprTuple(Forall(instance_param_or_params = sub_expr2, instance_expr = Equals(sub_expr13, sub_expr14), condition = sub_expr6), Equals(Lambda(sub_expr2, Conditional(sub_expr13, sub_expr6)), Lambda(sub_expr2, Conditional(sub_expr14, sub_expr6))).with_wrapping_at(2))

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_{s, t, U, \lvert u \rangle, \varphi~|~t \in \mathbb{N}^+}~\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..\right), \begin{array}{c} \begin{array}{l} \left[\left(s, t, U, \lvert u \rangle, \varphi\right) \mapsto \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.. \textrm{ if } t \in \mathbb{N}^+\right..\right] =  \\ \left[\left(s, t, U, \lvert u \rangle, \varphi\right) \mapsto \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..\right] \end{array} \end{array}\right)

stored_expr.style_options()

name	description	default	current value	related methods
wrap_positions	position(s) at which wrapping is to occur; 'n' is after the nth comma.	()	()	('with_wrapping_at',)
justification	if any wrap positions are set, justify to the 'left', 'center', or 'right'	left	left	('with_justification',)

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions	expression
0	ExprTuple	1, 2
1	Operation	operator: 3 operand: 6
2	Operation	operator: 38 operands: 5
3	Literal
4	ExprTuple	6
5	ExprTuple	7, 8
6	Lambda	parameters: 11 body: 9
7	Lambda	parameters: 11 body: 10
8	Lambda	parameters: 11 body: 12
9	Conditional	value: 13 condition: 14
10	Conditional	value: 17 condition: 14
11	ExprTuple	143, 151, 140, 129, 147
12	Conditional	value: 18 condition: 14
13	Operation	operator: 38 operands: 15
14	Operation	operator: 36 operands: 16
15	ExprTuple	17, 18
16	ExprTuple	151, 19
17	Conditional	value: 21 condition: 20
18	Conditional	value: 21 condition: 22
19	Literal
20	Operation	operator: 25 operands: 23
21	Operation	operator: 38 operands: 24
22	Operation	operator: 25 operands: 26
23	ExprTuple	29, 30, 31, 27
24	ExprTuple	28, 142
25	Literal
26	ExprTuple	29, 30, 31
27	Operation	operator: 36 operands: 32
28	Operation	operator: 33 operand: 41
29	Operation	operator: 36 operands: 35
30	Operation	operator: 36 operands: 37
31	Operation	operator: 38 operands: 39
32	ExprTuple	147, 40
33	Literal
34	ExprTuple	41
35	ExprTuple	147, 42
36	Literal
37	ExprTuple	141, 43
38	Literal
39	ExprTuple	44, 45
40	Operation	operator: 46 operands: 47
41	Operation	operator: 48 operands: 49
42	Literal
43	Operation	operator: 124 operands: 50
44	Operation	operator: 51 operands: 52
45	Operation	operator: 53 operands: 54
46	Literal
47	ExprTuple	59, 142
48	Literal
49	ExprTuple	55, 56, 57, 58
50	ExprTuple	59, 60
51	Literal
52	ExprTuple	140, 129
53	Literal
54	ExprTuple	61, 129
55	ExprTuple	62, 63
56	ExprTuple	64, 65
57	ExprTuple	66, 67
58	ExprTuple	68, 69
59	Literal
60	Operation	operator: 138 operands: 70
61	Operation	operator: 148 operands: 71
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