Expression of type Forall ¶

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, ExprRange, U, Variable, VertExprArray, s, t
from proveit.linear_algebra import MatrixMult, ScalarMult
from proveit.logic import And, Equals, Forall, InSet
from proveit.numbers import Add, Exp, Interval, IntervalCO, Mult, NaturalPos, Real, e, i, one, pi, subtract, two, zero
from proveit.physics.quantum import I, NumKet, Z, ket_plus, var_ket_u
from proveit.physics.quantum.QPE import QPE, phase, two_pow_t
from proveit.physics.quantum.circuits import Gate, Input, Measure, MultiQubitElem, Output, Qcircuit
from proveit.statistics import Prob

# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = Add(t, one)
sub_expr3 = Add(t, s)
sub_expr4 = InSet(phase, Real)
sub_expr5 = Interval(sub_expr2, sub_expr3)
sub_expr6 = Mult(two_pow_t, phase)
sub_expr7 = MultiQubitElem(element = Gate(operation = QPE(U, t), part = sub_expr1), targets = Interval(one, sub_expr3))
sub_expr8 = InSet(sub_expr6, Interval(zero, subtract(two_pow_t, one)))
sub_expr9 = Equals(MatrixMult(U, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, phase)), var_ket_u))
sub_expr10 = Equals(Prob(Qcircuit(vert_expr_array = VertExprArray([ExprRange(sub_expr1, Input(state = ket_plus), one, t), ExprRange(sub_expr1, MultiQubitElem(element = Input(state = var_ket_u, part = sub_expr1), targets = sub_expr5), one, s)], [ExprRange(sub_expr1, sub_expr7, one, t), ExprRange(sub_expr1, sub_expr7, sub_expr2, sub_expr3)], [ExprRange(sub_expr1, Measure(basis = Z), one, t), ExprRange(sub_expr1, Gate(operation = I).with_implicit_representation(), one, s)], [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(sub_expr6, t), part = sub_expr1), targets = Interval(one, t)), one, t), ExprRange(sub_expr1, MultiQubitElem(element = Output(state = var_ket_u, part = sub_expr1), targets = sub_expr5), one, s)]))), one)
expr = Forall(instance_param_or_params = [s, t, U, var_ket_u, phase], instance_expr = Equals(Conditional(sub_expr10, And(sub_expr4, sub_expr8, sub_expr9, InSet(phase, IntervalCO(zero, one)))), Conditional(sub_expr10, And(sub_expr4, sub_expr8, sub_expr9))).with_wrapping_at(1), condition = InSet(t, NaturalPos))

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

\forall_{s, t, U, \lvert u \rangle, \varphi~|~t \in \mathbb{N}^+}~\left(\begin{array}{c} \begin{array}{l} \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 2^{t} \cdot \varphi \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert 2^{t} \cdot \varphi \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 2^{t} \cdot \varphi \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert 2^{t} \cdot \varphi \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right) = 1 \textrm{ if } \varphi \in \mathbb{R} ,  \left(2^{t} \cdot \varphi\right) \in \{0~\ldotp \ldotp~2^{t} - 1\} ,  \left(U \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi} \cdot \lvert u \rangle\right) ,  \varphi \in \left[0,1\right)\right.. \\  = \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 2^{t} \cdot \varphi \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert 2^{t} \cdot \varphi \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 2^{t} \cdot \varphi \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert 2^{t} \cdot \varphi \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right) = 1 \textrm{ if } \varphi \in \mathbb{R} ,  \left(2^{t} \cdot \varphi\right) \in \{0~\ldotp \ldotp~2^{t} - 1\} ,  \left(U \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi} \cdot \lvert u \rangle\right)\right.. \end{array} \end{array}\right)

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

name	description	default	current value	related methods
with_wrapping	If 'True', wrap the Expression after the parameters	None	None/False	('with_wrapping',)
condition_wrapping	Wrap 'before' or 'after' the condition (or None).	None	None/False	('with_wrap_after_condition', 'with_wrap_before_condition')
wrap_params	If 'True', wraps every two parameters AND wraps the Expression after the parameters	None	None/False	('with_params',)
justification	justify to the 'left', 'center', or 'right' in the array cells	center	center	('with_justification',)

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

Expression of type Forall¶

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

Expression of type Forall ¶

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