logo

Theorems (or conjectures) for the theory of proveit.physics.quantum.QFT

In [1]:
import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import j, k, l, n
from proveit.linear_algebra import MatrixMult, Unitary
from proveit.logic import Equals, Forall, InSet
from proveit.numbers import zero, one, two, e, i, pi
from proveit.numbers import Exp, frac, Interval, Mult, Neg, sqrt, subtract
from proveit.numbers import NaturalPos
from proveit.physics.quantum import NumKet, NumBra, Qmult
from proveit.physics.quantum.QFT import FourierTransform, InverseFourierTransform
In [2]:
%begin theorems

Defining theorems for theory 'proveit.physics.quantum.QFT'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions
In [3]:
invFT_is_unitary = Forall(
    n,
    InSet(InverseFourierTransform(n), Unitary(Exp(two, n))),
    domain=NaturalPos)
invFT_is_unitary (conjecture without proof):
In [4]:
FT_on_matrix_elem = Forall(
    n,
    Forall((j, k),
           Equals(Qmult(NumBra(k, n),
                        FourierTransform(n),
                        NumKet(j, n)),
                  Qmult(frac(one, Exp(two, frac(n, two))),
                        Exp(e, frac(Mult(two, pi, i, j, k),
                                    Exp(two, n))))),
           domain=Interval(zero, subtract(Exp(two, n), one))),
    domain=NaturalPos)
FT_on_matrix_elem (conjecture without proof):
In [5]:
invFT_on_matrix_elem = Forall(
    n,
    Forall((k, l),
           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)),
                                   Exp(two, n))))),
           domain=Interval(zero, subtract(Exp(two, n), one))),
    domain=NaturalPos)
invFT_on_matrix_elem (conjecture without proof):
In [6]:
%end theorems

These theorems may now be imported from the theory package: proveit.physics.quantum.QFT