Expression of type ProbOfAll ¶

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 ExprRange, Variable, VertExprArray, e, l
from proveit.numbers import Add, Interval, ModAbs, greater, one
from proveit.physics.quantum import NumKet, Z, ket_plus
from proveit.physics.quantum.QPE import ModAdd, QPE, _U, _b_floor, _full_domain, _ket_u, _s, _s_wire, _t, _two_pow_t
from proveit.physics.quantum.circuits import Gate, Input, Measure, MultiQubitElem, Output, Qcircuit
from proveit.statistics import ProbOfAll

# 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 = MultiQubitElem(element = Gate(operation = QPE(_U, _t), part = sub_expr1), targets = Interval(one, sub_expr3))
expr = ProbOfAll(instance_param_or_params = [l], instance_element = 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_expr4), one, _s)], [ExprRange(sub_expr1, sub_expr5, one, _t), ExprRange(sub_expr1, sub_expr5, sub_expr2, sub_expr3)], [ExprRange(sub_expr1, Measure(basis = Z), one, _t), _s_wire], [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(ModAdd(_b_floor, l), _t), part = sub_expr1), targets = Interval(one, _t)), one, _t), ExprRange(sub_expr1, MultiQubitElem(element = Output(state = _ket_u, part = sub_expr1), targets = sub_expr4), one, _s)])), domain = _full_domain, condition = greater(ModAbs(l, _two_pow_t), e))

# 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{Prob}_{l \in \{-2^{t - 1} + 1~\ldotp \ldotp~2^{t - 1}\}~|~\left|l\right|_{\textup{mod}\thinspace 2^{t}} > e}~\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \multigate{4}{\textrm{QPE}\left(U, t\right)} & \meter & \multiqout{3}{\lvert b_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert b_{\textit{f}} \oplus l \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 b_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert b_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right)

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

name	description	default	current value	related methods
with_wrapping	If 'True', wrap the Expression after the parameters	None	None/False	('with_wrapping',)
condition_wrapping	Wrap 'before' or 'after' the condition (or None).	None	None/False	('with_wrap_after_condition', 'with_wrap_before_condition')
wrap_params	If 'True', wraps every two parameters AND wraps the Expression after the parameters	None	None/False	('with_params',)
justification	justify to the 'left', 'center', or 'right' in the array cells	center	center	('with_justification',)

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

Expression of type ProbOfAll¶

from the theory of proveit.physics.quantum.QPE¶

Expression of type ProbOfAll ¶

from the theory of proveit.physics.quantum.QPE ¶