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 ExprRange, U, Variable, VertExprArray, s, t
from proveit.linear_algebra import MatrixMult, ScalarMult
from proveit.logic import Equals, Forall, InSet
from proveit.numbers import Add, Exp, Interval, Mult, Real, e, i, one, pi, subtract, two, zero
from proveit.physics.quantum import I, NumKet, Z, ket_plus, normalized_var_ket_u, var_ket_u
from proveit.physics.quantum.QPE import QPE, phase, s_ket_domain, 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 = Interval(sub_expr2, sub_expr3)
sub_expr5 = Mult(two_pow_t, phase)
sub_expr6 = MultiQubitElem(element = Gate(operation = QPE(U, t), part = sub_expr1), targets = Interval(one, sub_expr3))
expr = Forall(instance_param_or_params = [var_ket_u], instance_expr = Forall(instance_param_or_params = [phase], instance_expr = 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_expr4), one, s)], [ExprRange(sub_expr1, sub_expr6, one, t), ExprRange(sub_expr1, sub_expr6, 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_expr5, 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_expr4), one, s)]))), one), domain = Real, conditions = [InSet(sub_expr5, Interval(zero, subtract(two_pow_t, one))), Equals(MatrixMult(U, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, phase)), var_ket_u))]).with_wrapping(), domain = s_ket_domain, condition = normalized_var_ket_u).with_wrapping()

# 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}{l}\forall_{\lvert u \rangle \in \mathbb{C}^{2^{s}}~|~\left \|\lvert u \rangle\right \| = 1}~\\
\left[\begin{array}{l}\forall_{\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)}~\\
\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\right)\end{array}\right]\end{array}

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