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, IntervalCO, Mod, Mult, Real, Round, e, four, frac, greater, i, one, pi, 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 = Interval(sub_expr2, sub_expr3)
sub_expr5 = MultiQubitElem(element = Gate(operation = QPE(U, t), part = sub_expr1), targets = Interval(one, sub_expr3))
expr = Forall(instance_param_or_params = [phase], instance_expr = greater(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_expr5, one, t), ExprRange(sub_expr1, sub_expr5, 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(Mod(Round(Mult(two_pow_t, phase)), two_pow_t), 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)]))), frac(four, Exp(pi, two))), domain = Real, conditions = [InSet(phase, IntervalCO(zero, one)), Equals(MatrixMult(U, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, phase)), 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_{\varphi \in \mathbb{R}~|~\varphi \in \left[0,1\right), \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 round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \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 round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert round\left(2^{t} \cdot \varphi\right) ~\textup{mod}~ 2^{t} \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right) > \frac{4}{\pi^{2}}\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: 1 operand: 3
1	Literal
2	ExprTuple	3
3	Lambda	parameter: 135 body: 5
4	ExprTuple	135
5	Conditional	value: 6 condition: 7
6	Operation	operator: 8 operands: 9
7	Operation	operator: 10 operands: 11
8	Literal
9	ExprTuple	12, 13
10	Literal
11	ExprTuple	14, 15, 16
12	Operation	operator: 17 operands: 18
13	Operation	operator: 19 operand: 28
14	Operation	operator: 22 operands: 21
15	Operation	operator: 22 operands: 23
16	Operation	operator: 24 operands: 25
17	Literal
18	ExprTuple	26, 27
19	Literal
20	ExprTuple	28
21	ExprTuple	135, 29
22	Literal
23	ExprTuple	135, 30
24	Literal
25	ExprTuple	31, 32
26	Literal
27	Operation	operator: 136 operands: 33
28	Operation	operator: 34 operands: 35
29	Literal
30	Operation	operator: 36 operands: 37
31	Operation	operator: 38 operands: 39
32	Operation	operator: 40 operands: 41
33	ExprTuple	84, 138
34	Literal
35	ExprTuple	42, 43, 44, 45
36	Literal
37	ExprTuple	46, 124
38	Literal
39	ExprTuple	122, 111
40	Literal
41	ExprTuple	47, 111
42	ExprTuple	48, 49
43	ExprTuple	50, 51
44	ExprTuple	52, 53
45	ExprTuple	54, 55
46	Literal
47	Operation	operator: 136 operands: 56
48	ExprRange	lambda_map: 57 start_index: 124 end_index: 139
49	ExprRange	lambda_map: 58 start_index: 124 end_index: 125
50	ExprRange	lambda_map: 59 start_index: 124 end_index: 139
51	ExprRange	lambda_map: 59 start_index: 113 end_index: 114
52	ExprRange	lambda_map: 60 start_index: 124 end_index: 139
53	ExprRange	lambda_map: 61 start_index: 124 end_index: 125
54	ExprRange	lambda_map: 62 start_index: 124 end_index: 139
55	ExprRange	lambda_map: 63 start_index: 124 end_index: 125
56	ExprTuple	64, 65
57	Lambda	parameter: 112 body: 66
58	Lambda	parameter: 112 body: 67
59	Lambda	parameter: 112 body: 68
60	Lambda	parameter: 112 body: 69
61	Lambda	parameter: 112 body: 70
62	Lambda	parameter: 112 body: 71
63	Lambda	parameter: 112 body: 73
64	Literal
65	Operation	operator: 132 operands: 74
66	Operation	operator: 98 operands: 75
67	Operation	operator: 82 operands: 76
68	Operation	operator: 82 operands: 77
69	Operation	operator: 78 operands: 79
70	Operation	operator: 99 operands: 80
71	Operation	operator: 82 operands: 81
72	ExprTuple	112
73	Operation	operator: 82 operands: 83
74	ExprTuple	138, 84, 85, 135
75	NamedExprs	state: 86
76	NamedExprs	element: 87 targets: 95
77	NamedExprs	element: 88 targets: 89
78	Literal
79	NamedExprs	basis: 90
80	NamedExprs	operation: 91
81	NamedExprs	element: 92 targets: 93
82	Literal
83	NamedExprs	element: 94 targets: 95
84	Literal
85	Literal
86	Operation	operator: 96 operand: 108
87	Operation	operator: 98 operands: 105
88	Operation	operator: 99 operands: 100
89	Operation	operator: 106 operands: 101
90	Literal
91	Literal
92	Operation	operator: 104 operands: 102
93	Operation	operator: 106 operands: 103
94	Operation	operator: 104 operands: 105
95	Operation	operator: 106 operands: 107
96	Literal
97	ExprTuple	108
98	Literal
99	Literal
100	NamedExprs	operation: 109 part: 112
101	ExprTuple	124, 114
102	NamedExprs	state: 110 part: 112
103	ExprTuple	124, 139
104	Literal
105	NamedExprs	state: 111 part: 112
106	Literal
107	ExprTuple	113, 114
108	Literal
109	Operation	operator: 115 operands: 116
110	Operation	operator: 117 operands: 118
111	Variable
112	Variable
113	Operation	operator: 120 operands: 119
114	Operation	operator: 120 operands: 121
115	Literal
116	ExprTuple	122, 139
117	Literal
118	ExprTuple	123, 139
119	ExprTuple	139, 124
120	Literal
121	ExprTuple	139, 125
122	Variable
123	Operation	operator: 126 operands: 127
124	Literal
125	Variable
126	Literal
127	ExprTuple	128, 134
128	Operation	operator: 129 operand: 131
129	Literal
130	ExprTuple	131
131	Operation	operator: 132 operands: 133
132	Literal
133	ExprTuple	134, 135
134	Operation	operator: 136 operands: 137
135	Variable
136	Literal
137	ExprTuple	138, 139
138	Literal
139	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 ¶