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, Literal, Variable, VertExprArray, e, m
from proveit.numbers import Add, Exp, Interval, ModAbs, greater, one, subtract, two, zero
from proveit.physics.quantum import I, NumKet, Z, ket_plus
from proveit.physics.quantum.QPE import QPE
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(Literal("t", theory = "proveit.physics.quantum.QPE"), one)
sub_expr3 = Add(Literal("t", theory = "proveit.physics.quantum.QPE"), Literal("s", theory = "proveit.physics.quantum.QPE"))
sub_expr4 = Exp(two, Literal("t", theory = "proveit.physics.quantum.QPE"))
sub_expr5 = Interval(sub_expr2, sub_expr3)
sub_expr6 = MultiQubitElem(element = Gate(operation = QPE(Literal("U", theory = "proveit.physics.quantum.QPE"), Literal("t", theory = "proveit.physics.quantum.QPE")), part = sub_expr1), targets = Interval(one, sub_expr3))
expr = ProbOfAll(instance_param_or_params = [m], instance_element = Qcircuit(vert_expr_array = VertExprArray([ExprRange(sub_expr1, Input(state = ket_plus), one, Literal("t", theory = "proveit.physics.quantum.QPE")), ExprRange(sub_expr1, MultiQubitElem(element = Input(state = Literal("|u>", latex_format = r"\lvert u \rangle", theory = "proveit.physics.quantum.QPE"), part = sub_expr1), targets = sub_expr5), one, Literal("s", theory = "proveit.physics.quantum.QPE"))], [ExprRange(sub_expr1, sub_expr6, one, Literal("t", theory = "proveit.physics.quantum.QPE")), ExprRange(sub_expr1, sub_expr6, sub_expr2, sub_expr3)], [ExprRange(sub_expr1, Measure(basis = Z), one, Literal("t", theory = "proveit.physics.quantum.QPE")), ExprRange(sub_expr1, Gate(operation = I).with_implicit_representation(), one, Literal("s", theory = "proveit.physics.quantum.QPE"))], [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(m, Literal("t", theory = "proveit.physics.quantum.QPE")), part = sub_expr1), targets = Interval(one, Literal("t", theory = "proveit.physics.quantum.QPE"))), one, Literal("t", theory = "proveit.physics.quantum.QPE")), ExprRange(sub_expr1, MultiQubitElem(element = Output(state = Literal("|u>", latex_format = r"\lvert u \rangle", theory = "proveit.physics.quantum.QPE"), part = sub_expr1), targets = sub_expr5), one, Literal("s", theory = "proveit.physics.quantum.QPE"))])), domain = Interval(zero, subtract(sub_expr4, one)), condition = greater(ModAbs(subtract(m, Literal("b_{f}", latex_format = r"b_{\textit{f}}", theory = "proveit.physics.quantum.QPE")), sub_expr4), e)).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}} > 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 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: 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: 113 end_index: 114
19	ExprRange	lambda_map: 31 start_index: 113 end_index: 115
20	ExprRange	lambda_map: 32 start_index: 113 end_index: 114
21	ExprRange	lambda_map: 32 start_index: 95 end_index: 96
22	ExprRange	lambda_map: 33 start_index: 113 end_index: 114
23	ExprRange	lambda_map: 34 start_index: 113 end_index: 115
24	ExprRange	lambda_map: 35 start_index: 113 end_index: 114
25	ExprRange	lambda_map: 36 start_index: 113 end_index: 115
26	Literal
27	ExprTuple	112, 37
28	Literal
29	ExprTuple	38, 39
30	Lambda	parameter: 94 body: 40
31	Lambda	parameter: 94 body: 41
32	Lambda	parameter: 94 body: 42
33	Lambda	parameter: 94 body: 43
34	Lambda	parameter: 94 body: 44
35	Lambda	parameter: 94 body: 45
36	Lambda	parameter: 94 body: 47
37	Operation	operator: 85 operands: 48
38	Variable
39	Operation	operator: 49 operands: 50
40	Operation	operator: 77 operands: 51
41	Operation	operator: 58 operands: 52
42	Operation	operator: 58 operands: 53
43	Operation	operator: 54 operands: 55
44	Operation	operator: 78 operands: 56
45	Operation	operator: 58 operands: 57
46	ExprTuple	94
47	Operation	operator: 58 operands: 59
48	ExprTuple	60, 61
49	Literal
50	ExprTuple	62, 87
51	NamedExprs	state: 63
52	NamedExprs	element: 64 targets: 72
53	NamedExprs	element: 65 targets: 66
54	Literal
55	NamedExprs	basis: 67
56	NamedExprs	operation: 68
57	NamedExprs	element: 69 targets: 70
58	Literal
59	NamedExprs	element: 71 targets: 72
60	Literal
61	Operation	operator: 107 operands: 73
62	Operation	operator: 107 operands: 74
63	Operation	operator: 75 operand: 90
64	Operation	operator: 77 operands: 84
65	Operation	operator: 78 operands: 79
66	Operation	operator: 85 operands: 80
67	Literal
68	Literal
69	Operation	operator: 83 operands: 81
70	Operation	operator: 85 operands: 82
71	Operation	operator: 83 operands: 84
72	Operation	operator: 85 operands: 86
73	ExprTuple	87, 88
74	ExprTuple	112, 89
75	Literal
76	ExprTuple	90
77	Literal
78	Literal
79	NamedExprs	operation: 91 part: 94
80	ExprTuple	113, 96
81	NamedExprs	state: 92 part: 94
82	ExprTuple	113, 114
83	Literal
84	NamedExprs	state: 93 part: 94
85	Literal
86	ExprTuple	95, 96
87	Operation	operator: 97 operands: 98
88	Operation	operator: 100 operand: 113
89	Operation	operator: 100 operand: 110
90	Literal
91	Operation	operator: 102 operands: 103
92	Operation	operator: 104 operands: 105
93	Literal
94	Variable
95	Operation	operator: 107 operands: 106
96	Operation	operator: 107 operands: 108
97	Literal
98	ExprTuple	109, 114
99	ExprTuple	113
100	Literal
101	ExprTuple	110
102	Literal
103	ExprTuple	111, 114
104	Literal
105	ExprTuple	112, 114
106	ExprTuple	114, 113
107	Literal
108	ExprTuple	114, 115
109	Literal
110	Literal
111	Literal
112	Variable
113	Literal
114	Literal
115	Literal