Expression of type Conditional ¶

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 Conditional, k, t
from proveit.linear_algebra import ScalarMult, VecSum
from proveit.logic import And, Equals, InSet
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 = Conditional(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))))), And(InSet(t, NaturalPos), 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())

\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) \textrm{ if } 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)\right..

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

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

Expression of type Conditional¶

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

Expression of type Conditional ¶

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