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 e, m
from proveit.logic import SetOfAll
from proveit.numbers import ModAbs, greater, subtract
from proveit.physics.quantum.QPE import _b_floor, _m_domain, _phase_est_circuit, _two_pow_t
from proveit.statistics import Prob

# build up the expression from sub-expressions
expr = Prob(SetOfAll(instance_param_or_params = [m], instance_element = _phase_est_circuit, domain = _m_domain, condition = greater(ModAbs(subtract(m, _b_floor), _two_pow_t), e)))

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(\left\{\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \multigate{4}{\textrm{QPE}\left(U, t\right)} & \meter & \multiqout{3}{\lvert m \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert m \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 m \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert m \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right)~|~\left|m - b_{\textit{f}}\right|_{\textup{mod}\thinspace 2^{t}} > e\right\}_{m \in \{0~\ldotp \ldotp~2^{t} - 1\}}\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 operand: 6
4	Literal
5	ExprTuple	6
6	Lambda	parameter: 115 body: 8
7	ExprTuple	115
8	Conditional	value: 9 condition: 10
9	Operation	operator: 11 operands: 12
10	Operation	operator: 13 operands: 14
11	Literal
12	ExprTuple	15, 16, 17, 18
13	Literal
14	ExprTuple	19, 20
15	ExprTuple	21, 22
16	ExprTuple	23, 24
17	ExprTuple	25, 26
18	ExprTuple	27, 28
19	Operation	operator: 29 operands: 30
20	Operation	operator: 31 operands: 32
21	ExprRange	lambda_map: 33 start_index: 116 end_index: 117
22	ExprRange	lambda_map: 34 start_index: 116 end_index: 118
23	ExprRange	lambda_map: 35 start_index: 116 end_index: 117
24	ExprRange	lambda_map: 35 start_index: 98 end_index: 99
25	ExprRange	lambda_map: 36 start_index: 116 end_index: 117
26	ExprRange	lambda_map: 37 start_index: 116 end_index: 118
27	ExprRange	lambda_map: 38 start_index: 116 end_index: 117
28	ExprRange	lambda_map: 39 start_index: 116 end_index: 118
29	Literal
30	ExprTuple	115, 40
31	Literal
32	ExprTuple	41, 42
33	Lambda	parameter: 97 body: 43
34	Lambda	parameter: 97 body: 44
35	Lambda	parameter: 97 body: 45
36	Lambda	parameter: 97 body: 46
37	Lambda	parameter: 97 body: 47
38	Lambda	parameter: 97 body: 48
39	Lambda	parameter: 97 body: 50
40	Operation	operator: 88 operands: 51
41	Variable
42	Operation	operator: 52 operands: 53
43	Operation	operator: 80 operands: 54
44	Operation	operator: 61 operands: 55
45	Operation	operator: 61 operands: 56
46	Operation	operator: 57 operands: 58
47	Operation	operator: 81 operands: 59
48	Operation	operator: 61 operands: 60
49	ExprTuple	97
50	Operation	operator: 61 operands: 62
51	ExprTuple	63, 64
52	Literal
53	ExprTuple	65, 90
54	NamedExprs	state: 66
55	NamedExprs	element: 67 targets: 75
56	NamedExprs	element: 68 targets: 69
57	Literal
58	NamedExprs	basis: 70
59	NamedExprs	operation: 71
60	NamedExprs	element: 72 targets: 73
61	Literal
62	NamedExprs	element: 74 targets: 75
63	Literal
64	Operation	operator: 110 operands: 76
65	Operation	operator: 110 operands: 77
66	Operation	operator: 78 operand: 93
67	Operation	operator: 80 operands: 87
68	Operation	operator: 81 operands: 82
69	Operation	operator: 88 operands: 83
70	Literal
71	Literal
72	Operation	operator: 86 operands: 84
73	Operation	operator: 88 operands: 85
74	Operation	operator: 86 operands: 87
75	Operation	operator: 88 operands: 89
76	ExprTuple	90, 91
77	ExprTuple	115, 92
78	Literal
79	ExprTuple	93
80	Literal
81	Literal
82	NamedExprs	operation: 94 part: 97
83	ExprTuple	116, 99
84	NamedExprs	state: 95 part: 97
85	ExprTuple	116, 117
86	Literal
87	NamedExprs	state: 96 part: 97
88	Literal
89	ExprTuple	98, 99
90	Operation	operator: 100 operands: 101
91	Operation	operator: 103 operand: 116
92	Operation	operator: 103 operand: 113
93	Literal
94	Operation	operator: 105 operands: 106
95	Operation	operator: 107 operands: 108
96	Literal
97	Variable
98	Operation	operator: 110 operands: 109
99	Operation	operator: 110 operands: 111
100	Literal
101	ExprTuple	112, 117
102	ExprTuple	116
103	Literal
104	ExprTuple	113
105	Literal
106	ExprTuple	114, 117
107	Literal
108	ExprTuple	115, 117
109	ExprTuple	117, 116
110	Literal
111	ExprTuple	117, 118
112	Literal
113	Literal
114	Literal
115	Variable
116	Literal
117	Literal
118	Literal