Expression of type Implies ¶

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

In [1]:

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 Equals, Forall, Implies, TRUE
from proveit.numbers import LessEq, ModAbs, one, subtract
from proveit.physics.quantum.QPE import Pfail, _b_floor, _m_domain, _phase_est_circuit, _two_pow_t
from proveit.statistics import ProbOfAll

In [2]:

# build up the expression from sub-expressions
sub_expr1 = [m]
expr = Implies(Forall(instance_param_or_params = sub_expr1, instance_expr = TRUE, domain = _m_domain), Equals(ProbOfAll(instance_param_or_params = sub_expr1, instance_element = _phase_est_circuit, domain = _m_domain, condition = LessEq(ModAbs(subtract(m, _b_floor), _two_pow_t), e)), subtract(one, Pfail(e))).with_wrapping_at(2)).with_wrapping_at(2)

expr:

In [3]:

# 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

In [4]:

# 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\}}~\top\right] \Rightarrow  \\ \left(\begin{array}{c} \begin{array}{l} \left[\textrm{Prob}_{m \in \{0~\ldotp \ldotp~2^{t} - 1\}~|~\left|m - b_{\textit{f}}\right|_{\textup{mod}\thinspace 2^{t}} \leq 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)\right] =  \\ \left(1 - \left[P_{\rm fail}\right]\left(e\right)\right) \end{array} \end{array}\right) \end{array} \end{array}

In [5]:

stored_expr.style_options()

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

In [6]:

# display the expression information
stored_expr.expr_info()

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