Expression of type Implies ¶

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, IndexedVar, Variable, VertExprArray, e, m
from proveit.logic import Forall, Implies, SetOfAll, SubsetEq, TRUE
from proveit.numbers import Add, Interval, ModAbs, greater, one, subtract
from proveit.physics.quantum import NumKet, Z, ket_plus
from proveit.physics.quantum.QPE import QPE, _U, _b_floor, _ket_u, _m_domain, _phase_est_circuit, _s, _s_wire, _t, _two_pow_t
from proveit.physics.quantum.circuits import Gate, Input, Measure, MultiQubitElem, Output, Qcircuit

# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = [m]
sub_expr3 = IndexedVar(m, one)
sub_expr4 = Add(_t, one)
sub_expr5 = Add(_t, _s)
sub_expr6 = Interval(sub_expr4, sub_expr5)
sub_expr7 = MultiQubitElem(element = Gate(operation = QPE(_U, _t), part = sub_expr1), targets = Interval(one, sub_expr5))
sub_expr8 = greater(ModAbs(subtract(m, _b_floor), _two_pow_t), e)
expr = Implies(Forall(instance_param_or_params = sub_expr2, instance_expr = TRUE, domain = _m_domain, condition = sub_expr8), SubsetEq(SetOfAll(instance_param_or_params = sub_expr2, instance_element = _phase_est_circuit, domain = _m_domain, condition = sub_expr8), SetOfAll(instance_param_or_params = [sub_expr3], instance_element = Qcircuit(vert_expr_array = VertExprArray([ExprRange(sub_expr1, Input(state = ket_plus), one, _t), ExprRange(sub_expr1, MultiQubitElem(element = Input(state = _ket_u, part = sub_expr1), targets = sub_expr6), one, _s)], [ExprRange(sub_expr1, sub_expr7, one, _t), ExprRange(sub_expr1, sub_expr7, sub_expr4, sub_expr5)], [ExprRange(sub_expr1, Measure(basis = Z), one, _t), _s_wire], [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(sub_expr3, _t), part = sub_expr1), targets = Interval(one, _t)), one, _t), ExprRange(sub_expr1, MultiQubitElem(element = Output(state = _ket_u, part = sub_expr1), targets = sub_expr6), one, _s)])), domain = _m_domain)).with_wrapping_at(2)).with_wrapping_at(2)

# 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}{c} \begin{array}{l} \left[\forall_{m \in \{0~\ldotp \ldotp~2^{t} - 1\}~|~\left|m - b_{\textit{f}}\right|_{\textup{mod}\thinspace 2^{t}} > e}~\top\right] \Rightarrow  \\ \left(\begin{array}{c} \begin{array}{l} \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_{1} \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert m_{1} \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_{1} \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert m_{1} \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right\}_{m_{1} \in \{0~\ldotp \ldotp~2^{t} - 1\}} \end{array} \end{array}\right) \end{array} \end{array}

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.	()	(2)	('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: 5 operand: 9
4	Operation	operator: 7 operands: 8
5	Literal
6	ExprTuple	9
7	Literal
8	ExprTuple	10, 11
9	Lambda	parameter: 144 body: 12
10	Operation	operator: 14 operand: 17
11	Operation	operator: 14 operand: 18
12	Conditional	value: 16 condition: 24
13	ExprTuple	17
14	Literal
15	ExprTuple	18
16	Literal
17	Lambda	parameter: 144 body: 20
18	Lambda	parameter: 141 body: 22
19	ExprTuple	144
20	Conditional	value: 23 condition: 24
21	ExprTuple	141
22	Conditional	value: 25 condition: 26
23	Operation	operator: 30 operands: 27
24	Operation	operator: 28 operands: 29
25	Operation	operator: 30 operands: 31
26	Operation	operator: 41 operands: 32
27	ExprTuple	36, 37, 38, 33
28	Literal
29	ExprTuple	34, 35
30	Literal
31	ExprTuple	36, 37, 38, 39
32	ExprTuple	141, 54
33	ExprTuple	40, 52
34	Operation	operator: 41 operands: 42
35	Operation	operator: 43 operands: 44
36	ExprTuple	45, 46
37	ExprTuple	47, 48
38	ExprTuple	49, 50
39	ExprTuple	51, 52
40	ExprRange	lambda_map: 53 start_index: 146 end_index: 142
41	Literal
42	ExprTuple	144, 54
43	Literal
44	ExprTuple	55, 56
45	ExprRange	lambda_map: 57 start_index: 146 end_index: 142
46	ExprRange	lambda_map: 58 start_index: 146 end_index: 143
47	ExprRange	lambda_map: 59 start_index: 146 end_index: 142
48	ExprRange	lambda_map: 59 start_index: 128 end_index: 129
49	ExprRange	lambda_map: 60 start_index: 146 end_index: 142
50	ExprRange	lambda_map: 61 start_index: 146 end_index: 143
51	ExprRange	lambda_map: 62 start_index: 146 end_index: 142
52	ExprRange	lambda_map: 63 start_index: 146 end_index: 143
53	Lambda	parameter: 127 body: 64
54	Operation	operator: 116 operands: 65
55	Variable
56	Operation	operator: 66 operands: 67
57	Lambda	parameter: 127 body: 68
58	Lambda	parameter: 127 body: 69
59	Lambda	parameter: 127 body: 70
60	Lambda	parameter: 127 body: 71
61	Lambda	parameter: 127 body: 72
62	Lambda	parameter: 127 body: 73
63	Lambda	parameter: 127 body: 75
64	Operation	operator: 87 operands: 76
65	ExprTuple	77, 78
66	Literal
67	ExprTuple	79, 103
68	Operation	operator: 108 operands: 80
69	Operation	operator: 87 operands: 81
70	Operation	operator: 87 operands: 82
71	Operation	operator: 83 operands: 84
72	Operation	operator: 109 operands: 85
73	Operation	operator: 87 operands: 86
74	ExprTuple	127
75	Operation	operator: 87 operands: 88
76	NamedExprs	element: 89 targets: 99
77	Literal
78	Operation	operator: 138 operands: 90
79	Operation	operator: 138 operands: 91
80	NamedExprs	state: 92
81	NamedExprs	element: 93 targets: 101
82	NamedExprs	element: 94 targets: 95
83	Literal
84	NamedExprs	basis: 96
85	NamedExprs	operation: 97
86	NamedExprs	element: 98 targets: 99
87	Literal
88	NamedExprs	element: 100 targets: 101
89	Operation	operator: 114 operands: 102
90	ExprTuple	103, 104
91	ExprTuple	144, 105
92	Operation	operator: 106 operand: 123
93	Operation	operator: 108 operands: 115
94	Operation	operator: 109 operands: 110
95	Operation	operator: 116 operands: 111
96	Literal
97	Literal
98	Operation	operator: 114 operands: 112
99	Operation	operator: 116 operands: 113
100	Operation	operator: 114 operands: 115
101	Operation	operator: 116 operands: 117
102	NamedExprs	state: 118 part: 127
103	Operation	operator: 119 operands: 120
104	Operation	operator: 121 operand: 146
105	Operation	operator: 121 operand: 132
106	Literal
107	ExprTuple	123
108	Literal
109	Literal
110	NamedExprs	operation: 124 part: 127
111	ExprTuple	146, 129
112	NamedExprs	state: 125 part: 127
113	ExprTuple	146, 142
114	Literal
115	NamedExprs	state: 126 part: 127
116	Literal
117	ExprTuple	128, 129
118	Operation	operator: 135 operands: 130
119	Literal
120	ExprTuple	131, 142
121	Literal
122	ExprTuple	132
123	Literal
124	Operation	operator: 133 operands: 134
125	Operation	operator: 135 operands: 136
126	Literal
127	Variable
128	Operation	operator: 138 operands: 137
129	Operation	operator: 138 operands: 139
130	ExprTuple	144, 142
131	Literal
132	Literal
133	Literal
134	ExprTuple	140, 142
135	Literal
136	ExprTuple	141, 142
137	ExprTuple	142, 146
138	Literal
139	ExprTuple	142, 143
140	Literal
141	IndexedVar	variable: 144 index: 146
142	Literal
143	Literal
144	Variable
145	ExprTuple	146
146	Literal

Expression of type Implies¶

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

Expression of type Implies ¶

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