Expression of type Conditional ¶

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

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, l, n
from proveit.logic import Equals, Forall, InSet
from proveit.numbers import Exp, Interval, Mult, NaturalPos, Neg, e, frac, i, one, pi, subtract, two, zero
from proveit.physics.quantum import NumBra, NumKet, Qmult
from proveit.physics.quantum.QFT import InverseFourierTransform

# build up the expression from sub-expressions
sub_expr1 = Exp(two, n)
expr = Conditional(Forall(instance_param_or_params = [k, l], instance_expr = Equals(Qmult(NumBra(l, n), InverseFourierTransform(n), NumKet(k, n)), Mult(frac(one, Exp(two, frac(n, two))), Exp(e, frac(Neg(Mult(two, pi, i, k, l)), sub_expr1)))), domain = Interval(zero, subtract(sub_expr1, one))), InSet(n, 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\{\forall_{k, l \in \{0~\ldotp \ldotp~2^{n} - 1\}}~\left(\left({_{n}}\langle l \rvert \thinspace {\mathrm {FT}}^{\dag}_{n} \thinspace \lvert k \rangle_{n}\right) = \left(\frac{1}{2^{\frac{n}{2}}} \cdot \mathsf{e}^{\frac{-\left(2 \cdot \pi \cdot \mathsf{i} \cdot k \cdot l\right)}{2^{n}}}\right)\right) \textrm{ if } n \in \mathbb{N}^+\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: 3 operand: 6
2	Operation	operator: 24 operands: 5
3	Literal
4	ExprTuple	6
5	ExprTuple	63, 7
6	Lambda	parameters: 8 body: 9
7	Literal
8	ExprTuple	70, 71
9	Conditional	value: 10 condition: 11
10	Operation	operator: 12 operands: 13
11	Operation	operator: 14 operands: 15
12	Literal
13	ExprTuple	16, 17
14	Literal
15	ExprTuple	18, 19
16	Operation	operator: 20 operands: 21
17	Operation	operator: 65 operands: 22
18	Operation	operator: 24 operands: 23
19	Operation	operator: 24 operands: 25
20	Literal
21	ExprTuple	26, 27, 28
22	ExprTuple	29, 30
23	ExprTuple	70, 31
24	Literal
25	ExprTuple	71, 31
26	Operation	operator: 32 operands: 33
27	Operation	operator: 34 operand: 63
28	Operation	operator: 36 operands: 37
29	Operation	operator: 55 operands: 38
30	Operation	operator: 58 operands: 39
31	Operation	operator: 40 operands: 41
32	Literal
33	ExprTuple	71, 63
34	Literal
35	ExprTuple	63
36	Literal
37	ExprTuple	70, 63
38	ExprTuple	64, 42
39	ExprTuple	43, 44
40	Literal
41	ExprTuple	45, 46
42	Operation	operator: 58 operands: 47
43	Literal
44	Operation	operator: 55 operands: 48
45	Literal
46	Operation	operator: 49 operands: 50
47	ExprTuple	67, 51
48	ExprTuple	52, 53
49	Literal
50	ExprTuple	53, 54
51	Operation	operator: 55 operands: 56
52	Operation	operator: 60 operand: 62
53	Operation	operator: 58 operands: 59
54	Operation	operator: 60 operand: 64
55	Literal
56	ExprTuple	63, 67
57	ExprTuple	62
58	Literal
59	ExprTuple	67, 63
60	Literal
61	ExprTuple	64
62	Operation	operator: 65 operands: 66
63	Variable
64	Literal
65	Literal
66	ExprTuple	67, 68, 69, 70, 71
67	Literal
68	Literal
69	Literal
70	Variable
71	Variable

Expression of type Conditional¶

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

Expression of type Conditional ¶

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