Expression of type Prob

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, ConditionalSet, ExprRange, Variable, VertExprArray, t
from proveit.linear_algebra import MatrixExp, ScalarMult, VecAdd
from proveit.logic import Equals, NotEquals, Set
from proveit.numbers import Add, Exp, Interval, Mult, Neg, e, frac, i, one, pi, sqrt, two, zero
from proveit.physics.quantum import CONTROL, ket0, ket1, ket_plus
from proveit.physics.quantum.QPE import _U, _ket_u, _phase, _s
from proveit.physics.quantum.circuits import Gate, Igate, Input, 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 = Variable("_b", latex_format = r"{_{-}b}")
sub_expr3 = Add(t, one)
sub_expr4 = Add(sub_expr2, t)
sub_expr5 = Interval(sub_expr3, Add(t, _s))
sub_expr6 = Add(Neg(t), one)
expr = Prob(Qcircuit(vert_expr_array = VertExprArray([ExprRange(sub_expr1, Input(state = ket_plus), one, t), ExprRange(sub_expr1, MultiQubitElem(element = Input(state = _ket_u, part = sub_expr1), targets = sub_expr5), one, _s)], ExprRange(sub_expr2, [ExprRange(sub_expr1, ConditionalSet(Conditional(MultiQubitElem(element = CONTROL, targets = Set(sub_expr3)), Equals(sub_expr4, sub_expr1)), Conditional(Igate, NotEquals(sub_expr4, sub_expr1))), one, t).with_case_simplification(), ExprRange(sub_expr1, MultiQubitElem(element = Gate(operation = MatrixExp(_U, Exp(two, Neg(sub_expr2))), part = sub_expr1), targets = sub_expr5), one, _s)], sub_expr6, zero).with_decreasing_order(), [ExprRange(sub_expr1, Output(state = ScalarMult(frac(one, sqrt(two)), VecAdd(ket0, ScalarMult(Exp(e, Mult(two, pi, i, Exp(two, Neg(sub_expr1)), _phase)), ket1)))), sub_expr6, zero).with_decreasing_order(), ExprRange(sub_expr1, MultiQubitElem(element = Output(state = _ket_u, part = sub_expr1), targets = sub_expr5), one, _s)])))

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())

\textrm{Pr}\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \control{} \qw \qwx[1] & \qw & \gate{\cdots} \qwx[1] & \qw & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot 2^{t - 1} \cdot \varphi} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\lvert + \rangle} & \qw \qwx[1] & \control{} \qw \qwx[1] & \gate{\cdots} \qwx[1] & \qw & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot 2^{t - 2} \cdot \varphi} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} & \gate{\vdots} \qwx[1] & \gate{\vdots} \qwx[1] & \gate{\ddots} \qwx[1] & \gate{\vdots} & \qout{\vdots} \\
\qin{\lvert + \rangle} & \qw \qwx[1] & \qw \qwx[1] & \gate{\cdots} \qwx[1] & \control{} \qw \qwx[1] & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot 2^{0} \cdot \varphi} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\lvert u \rangle} & \gate{U^{2^{t - 1}}} & \gate{U^{2^{t - 2}}} & \gate{\cdots} & \gate{U^{2^{0}}} & \qout{\lvert u \rangle}
} \end{array}\right)

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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