Expression of type SubsetEq ¶

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, SubsetEq
from proveit.numbers import ModAbs, greater, subtract
from proveit.physics.quantum.QPE import _b_floor, _m_domain, _phase_est_circuit, _sample_space, _two_pow_t

# build up the expression from sub-expressions
expr = SubsetEq(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)), _sample_space)

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

\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\}} \subseteq \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\}_{m \in \{0~\ldotp \ldotp~2^{t} - 1\}}

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

name	description	default	current value	related methods
operation	'infix' or 'function' style formatting	infix	infix
wrap_positions	position(s) at which wrapping is to occur; '2 n - 1' is after the nth operand, '2 n' is after the nth operation.	()	()	('with_wrapping_at', 'with_wrap_before_operator', 'with_wrap_after_operator', 'without_wrapping', 'wrap_positions')
justification	if any wrap positions are set, justify to the 'left', 'center', or 'right'	center	center	('with_justification',)
direction	Direction of the relation (normal or reversed)	normal	normal	('with_direction_reversed', 'is_reversed')

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

Expression of type SubsetEq¶

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

Expression of type SubsetEq ¶

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