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, 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 = 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 = [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()

# 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}~|~\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}

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