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.physics.quantum.QPE import _m_domain, _phase_est_circuit, _success_cond
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 = _success_cond).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|\frac{m}{2^{t}} - \varphi\right|_{\textup{mod}\thinspace 1} \leq 2^{-n}}~\\
\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: 116 body: 5
4	ExprTuple	116
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: 117 end_index: 122
19	ExprRange	lambda_map: 31 start_index: 117 end_index: 118
20	ExprRange	lambda_map: 32 start_index: 117 end_index: 122
21	ExprRange	lambda_map: 32 start_index: 99 end_index: 100
22	ExprRange	lambda_map: 33 start_index: 117 end_index: 122
23	ExprRange	lambda_map: 34 start_index: 117 end_index: 118
24	ExprRange	lambda_map: 35 start_index: 117 end_index: 122
25	ExprRange	lambda_map: 36 start_index: 117 end_index: 118
26	Literal
27	ExprTuple	116, 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: 119 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, 117
51	ExprTuple	121, 64
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: 104 operand: 93
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	113, 90
76	ExprTuple	91, 92
77	ExprTuple	93
78	Literal
79	ExprTuple	94
80	Literal
81	Literal
82	NamedExprs	operation: 95 part: 98
83	ExprTuple	117, 100
84	NamedExprs	state: 96 part: 98
85	ExprTuple	117, 122
86	Literal
87	NamedExprs	state: 97 part: 98
88	Literal
89	ExprTuple	99, 100
90	Operation	operator: 104 operand: 117
91	Operation	operator: 102 operands: 103
92	Operation	operator: 104 operand: 114
93	Literal
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	ExprTuple	117
102	Literal
103	ExprTuple	116, 113
104	Literal
105	ExprTuple	114
106	Literal
107	ExprTuple	115, 122
108	Literal
109	ExprTuple	116, 122
110	ExprTuple	122, 117
111	Literal
112	ExprTuple	122, 118
113	Operation	operator: 119 operands: 120
114	Literal
115	Literal
116	Variable
117	Literal
118	Literal
119	Literal
120	ExprTuple	121, 122
121	Literal
122	Literal