Expression of type Implies ¶

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 k, t
from proveit.linear_algebra import ScalarMult, VecSum
from proveit.logic import And, Equals, Forall, Implies
from proveit.numbers import Add, Exp, Interval, Mult, NaturalPos, e, frac, i, one, pi, sqrt, subtract, two, zero
from proveit.physics.quantum import Ket, NumKet
from proveit.physics.quantum.QPE import SubIndexed, _phase, _psi, _psi_t_ket, two_pow_t

# build up the expression from sub-expressions
sub_expr1 = [k]
sub_expr2 = [t]
sub_expr3 = Add(t, one)
sub_expr4 = Exp(e, Mult(two, pi, i, _phase, k))
sub_expr5 = Equals(_psi_t_ket, ScalarMult(frac(one, Exp(two, frac(t, two))), VecSum(index_or_indices = sub_expr1, summand = ScalarMult(sub_expr4, NumKet(k, t)), domain = Interval(zero, subtract(two_pow_t, one)))))
expr = Implies(And(Equals(SubIndexed(_psi, [one]), ScalarMult(frac(one, sqrt(two)), VecSum(index_or_indices = sub_expr1, summand = ScalarMult(sub_expr4, Ket(k)), domain = Interval(zero, one)))), Forall(instance_param_or_params = sub_expr2, instance_expr = Equals(SubIndexed(_psi, [sub_expr3]), ScalarMult(frac(one, Exp(two, frac(sub_expr3, two))), VecSum(index_or_indices = sub_expr1, summand = ScalarMult(sub_expr4, NumKet(k, sub_expr3)), domain = Interval(zero, subtract(Mult(two, two_pow_t), one))))), domain = NaturalPos, condition = sub_expr5)), Forall(instance_param_or_params = sub_expr2, instance_expr = sub_expr5, domain = 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())

\left(\left(\lvert \psi_{1} \rangle = \left(\frac{1}{\sqrt{2}} \cdot \left(\sum_{k=0}^{1} \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi \cdot k} \cdot \lvert k \rangle\right)\right)\right)\right) \land \left[\forall_{t \in \mathbb{N}^+~|~\lvert \psi_{t} \rangle = \left(\frac{1}{2^{\frac{t}{2}}} \cdot \left(\sum_{k=0}^{2^{t} - 1} \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi \cdot k} \cdot \lvert k \rangle_{t}\right)\right)\right)}~\left(\lvert \psi_{t + 1} \rangle = \left(\frac{1}{2^{\frac{t + 1}{2}}} \cdot \left(\sum_{k=0}^{\left(2 \cdot 2^{t}\right) - 1} \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi \cdot k} \cdot \lvert k \rangle_{t + 1}\right)\right)\right)\right)\right]\right) \Rightarrow \left[\forall_{t \in \mathbb{N}^+}~\left(\lvert \psi_{t} \rangle = \left(\frac{1}{2^{\frac{t}{2}}} \cdot \left(\sum_{k=0}^{2^{t} - 1} \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi \cdot k} \cdot \lvert k \rangle_{t}\right)\right)\right)\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',)
direction	Direction of the relation (normal or reversed)	normal	normal	('with_direction_reversed', 'is_reversed')

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

Expression of type Implies¶

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

Expression of type Implies ¶

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