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 m
from proveit.numbers import LessEq, ModAbs, subtract
from proveit.physics.quantum.QPE import _b_floor, _e_value, _m_domain, _phase_est_circuit, _two_pow_t
from proveit.statistics import ProbOfAll

# build up the expression from sub-expressions
expr = ProbOfAll(instance_param_or_params = [m], instance_element = _phase_est_circuit, domain = _m_domain, condition = LessEq(ModAbs(subtract(m, _b_floor), _two_pow_t), _e_value)).with_wrapping()

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

\begin{array}{l}\textrm{Prob}_{m \in \{0~\ldotp \ldotp~2^{t} - 1\}~|~\left|m - b_{\textit{f}}\right|_{\textup{mod}\thinspace 2^{t}} \leq \left(2^{t - n} - 1\right)}~\\
\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)\end{array}

stored_expr.style_options()

name	description	default	current value	related methods
with_wrapping	If 'True', wrap the Expression after the parameters	None	True	('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',)

# 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	Lambda	parameter: 117 body: 5
4	ExprTuple	117
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: 118 end_index: 119
19	ExprRange	lambda_map: 31 start_index: 118 end_index: 120
20	ExprRange	lambda_map: 32 start_index: 118 end_index: 119
21	ExprRange	lambda_map: 32 start_index: 99 end_index: 100
22	ExprRange	lambda_map: 33 start_index: 118 end_index: 119
23	ExprRange	lambda_map: 34 start_index: 118 end_index: 120
24	ExprRange	lambda_map: 35 start_index: 118 end_index: 119
25	ExprRange	lambda_map: 36 start_index: 118 end_index: 120
26	Literal
27	ExprTuple	117, 37
28	Literal
29	ExprTuple	38, 39
30	Lambda	parameter: 98 body: 40
31	Lambda	parameter: 98 body: 41
32	Lambda	parameter: 98 body: 42
33	Lambda	parameter: 98 body: 43
34	Lambda	parameter: 98 body: 44
35	Lambda	parameter: 98 body: 45
36	Lambda	parameter: 98 body: 47
37	Operation	operator: 88 operands: 48
38	Operation	operator: 49 operands: 50
39	Operation	operator: 111 operands: 51
40	Operation	operator: 80 operands: 52
41	Operation	operator: 59 operands: 53
42	Operation	operator: 59 operands: 54
43	Operation	operator: 55 operands: 56
44	Operation	operator: 81 operands: 57
45	Operation	operator: 59 operands: 58
46	ExprTuple	98
47	Operation	operator: 59 operands: 60
48	ExprTuple	61, 62
49	Literal
50	ExprTuple	63, 90
51	ExprTuple	64, 91
52	NamedExprs	state: 65
53	NamedExprs	element: 66 targets: 74
54	NamedExprs	element: 67 targets: 68
55	Literal
56	NamedExprs	basis: 69
57	NamedExprs	operation: 70
58	NamedExprs	element: 71 targets: 72
59	Literal
60	NamedExprs	element: 73 targets: 74
61	Literal
62	Operation	operator: 111 operands: 75
63	Operation	operator: 111 operands: 76
64	Operation	operator: 101 operands: 77
65	Operation	operator: 78 operand: 94
66	Operation	operator: 80 operands: 87
67	Operation	operator: 81 operands: 82
68	Operation	operator: 88 operands: 83
69	Literal
70	Literal
71	Operation	operator: 86 operands: 84
72	Operation	operator: 88 operands: 85
73	Operation	operator: 86 operands: 87
74	Operation	operator: 88 operands: 89
75	ExprTuple	90, 91
76	ExprTuple	117, 92
77	ExprTuple	113, 93
78	Literal
79	ExprTuple	94
80	Literal
81	Literal
82	NamedExprs	operation: 95 part: 98
83	ExprTuple	118, 100
84	NamedExprs	state: 96 part: 98
85	ExprTuple	118, 119
86	Literal
87	NamedExprs	state: 97 part: 98
88	Literal
89	ExprTuple	99, 100
90	Operation	operator: 101 operands: 102
91	Operation	operator: 121 operand: 118
92	Operation	operator: 121 operand: 114
93	Operation	operator: 111 operands: 105
94	Literal
95	Operation	operator: 106 operands: 107
96	Operation	operator: 108 operands: 109
97	Literal
98	Variable
99	Operation	operator: 111 operands: 110
100	Operation	operator: 111 operands: 112
101	Literal
102	ExprTuple	113, 119
103	ExprTuple	118
104	ExprTuple	114
105	ExprTuple	119, 115
106	Literal
107	ExprTuple	116, 119
108	Literal
109	ExprTuple	117, 119
110	ExprTuple	119, 118
111	Literal
112	ExprTuple	119, 120
113	Literal
114	Literal
115	Operation	operator: 121 operand: 123
116	Literal
117	Variable
118	Literal
119	Literal
120	Literal
121	Literal
122	ExprTuple	123
123	Literal