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 k, t
from proveit.linear_algebra import ScalarMult, VecSum
from proveit.logic import Equals, Forall
from proveit.numbers import Add, Exp, Interval, Mult, NaturalPos, e, frac, i, one, pi, subtract, two, zero
from proveit.physics.quantum import 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 = Add(t, one)
sub_expr3 = Exp(e, Mult(two, pi, i, _phase, k))
expr = Forall(instance_param_or_params = [t], instance_expr = Equals(SubIndexed(_psi, [sub_expr2]), ScalarMult(frac(one, Exp(two, frac(sub_expr2, two))), VecSum(index_or_indices = sub_expr1, summand = ScalarMult(sub_expr3, NumKet(k, sub_expr2)), domain = Interval(zero, subtract(Mult(two, two_pow_t), one))))), domain = NaturalPos, condition = Equals(_psi_t_ket, ScalarMult(frac(one, Exp(two, frac(t, two))), VecSum(index_or_indices = sub_expr1, summand = ScalarMult(sub_expr3, NumKet(k, t)), domain = Interval(zero, subtract(two_pow_t, one))))))

# 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_{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)

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	parameter: 95 body: 4
4	Conditional	value: 5 condition: 6
5	Operation	operator: 17 operands: 7
6	Operation	operator: 8 operands: 9
7	ExprTuple	10, 11
8	Literal
9	ExprTuple	12, 13
10	Operation	operator: 26 operand: 62
11	Operation	operator: 58 operands: 15
12	Operation	operator: 60 operands: 16
13	Operation	operator: 17 operands: 18
14	ExprTuple	62
15	ExprTuple	19, 20
16	ExprTuple	95, 21
17	Literal
18	ExprTuple	22, 23
19	Operation	operator: 56 operands: 24
20	Operation	operator: 36 operand: 30
21	Literal
22	Operation	operator: 26 operand: 95
23	Operation	operator: 58 operands: 28
24	ExprTuple	96, 29
25	ExprTuple	30
26	Literal
27	ExprTuple	95
28	ExprTuple	31, 32
29	Operation	operator: 90 operands: 33
30	Lambda	parameter: 87 body: 34
31	Operation	operator: 56 operands: 35
32	Operation	operator: 36 operand: 42
33	ExprTuple	94, 38
34	Conditional	value: 39 condition: 40
35	ExprTuple	96, 41
36	Literal
37	ExprTuple	42
38	Operation	operator: 56 operands: 43
39	Operation	operator: 58 operands: 44
40	Operation	operator: 60 operands: 45
41	Operation	operator: 90 operands: 46
42	Lambda	parameter: 87 body: 48
43	ExprTuple	62, 94
44	ExprTuple	64, 49
45	ExprTuple	87, 50
46	ExprTuple	94, 51
47	ExprTuple	87
48	Conditional	value: 52 condition: 53
49	Operation	operator: 70 operands: 54
50	Operation	operator: 72 operands: 55
51	Operation	operator: 56 operands: 57
52	Operation	operator: 58 operands: 59
53	Operation	operator: 60 operands: 61
54	ExprTuple	87, 62
55	ExprTuple	77, 63
56	Literal
57	ExprTuple	95, 94
58	Literal
59	ExprTuple	64, 65
60	Literal
61	ExprTuple	87, 66
62	Operation	operator: 82 operands: 67
63	Operation	operator: 82 operands: 68
64	Operation	operator: 90 operands: 69
65	Operation	operator: 70 operands: 71
66	Operation	operator: 72 operands: 73
67	ExprTuple	95, 96
68	ExprTuple	74, 89
69	ExprTuple	75, 76
70	Literal
71	ExprTuple	87, 95
72	Literal
73	ExprTuple	77, 78
74	Operation	operator: 80 operands: 79
75	Literal
76	Operation	operator: 80 operands: 81
77	Literal
78	Operation	operator: 82 operands: 83
79	ExprTuple	94, 88
80	Literal
81	ExprTuple	94, 84, 85, 86, 87
82	Literal
83	ExprTuple	88, 89
84	Literal
85	Literal
86	Literal
87	Variable
88	Operation	operator: 90 operands: 91
89	Operation	operator: 92 operand: 96
90	Literal
91	ExprTuple	94, 95
92	Literal
93	ExprTuple	96
94	Literal
95	Variable
96	Literal

Expression of type Forall¶

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

Expression of type Forall ¶

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