Expression of type And ¶

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 Lambda, m
from proveit.logic import And, InSet, Injections, Surjections
from proveit.physics.quantum.QPE import _Omega, _m_domain, _phase_est_circuit

# build up the expression from sub-expressions
sub_expr1 = Lambda(m, _phase_est_circuit)
expr = And(InSet(sub_expr1, Injections(_m_domain, _Omega)), InSet(sub_expr1, Surjections(_m_domain, _Omega)))

# 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[m \mapsto \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] \in \left[\{0~\ldotp \ldotp~2^{t} - 1\} \xrightarrow[]{\text{1-to-1}} \Omega\right]\right) \land \left(\left[m \mapsto \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] \in \left[\{0~\ldotp \ldotp~2^{t} - 1\} \xrightarrow[\text{onto}]{} \Omega\right]\right)

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

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

Expression of type And¶

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

Expression of type And ¶

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