Expression of type Conditional ¶

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 Conditional, m
from proveit.logic import Equals, InSet
from proveit.physics.quantum.QPE import _alpha_m_sqrd, _m_domain, _phase_est_circuit
from proveit.statistics import Prob

# build up the expression from sub-expressions
expr = Conditional(Equals(Prob(_phase_est_circuit), _alpha_m_sqrd), InSet(m, _m_domain))

# 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\{\textrm{Pr}\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|\alpha_{m}\right|^{2} \textrm{ if } m \in \{0~\ldotp \ldotp~2^{t} - 1\}\right..

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

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

Expression of type Conditional¶

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

Expression of type Conditional ¶

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