The Fourier transform #
We set up the Fourier transform for complex-valued functions on finite-dimensional spaces.
Design choices #
In namespace vector_fourier
, we define the Fourier integral in the following context:
π
is a commutative ring.V
andW
areπ
-modules.e
is a unitary additive character ofπ
, i.e. a homomorphism(multiplicative π) β* circle
.ΞΌ
is a measure onV
.L
is aπ
-bilinear formV Γ W β π
.E
is a complete normedβ
-vector space.
With these definitions, we define fourier_integral
to be the map from functions V β E
to
functions W β E
that sends f
to
Ξ» w, β« v in V, e [-L v w] β’ f v βΞΌ
,
where e [x]
is notational sugar for (e (multiplicative.of_add x) : β)
(available in locale
fourier_transform
). This includes the cases W
is the dual of V
and L
is the canonical
pairing, or W = V
and L
is a bilinear form (e.g. an inner product).
In namespace fourier
, we consider the more familiar special case when V = W = π
and L
is the
multiplication map (but still allowing π
to be an arbitrary ring equipped with a measure).
The most familiar case of all is when V = W = π = β
, L
is multiplication, ΞΌ
is volume, and
e
is real.fourier_char
, i.e. the character Ξ» x, exp ((2 * Ο * x) * I)
. The Fourier integral
in this case is defined as real.fourier_integral
.
Main results #
At present the only nontrivial lemma we prove is continuous_fourier_integral
, stating that the
Fourier transform of an integrable function is continuous (under mild assumptions).
Fourier theory for functions on general vector spaces #
The Fourier transform integral for f : V β E
, with respect to a bilinear form L : V Γ W β π
and an additive character e
.
The uniform norm of the Fourier integral of f
is bounded by the LΒΉ
norm of f
.
The Fourier integral converts right-translation into scalar multiplication by a phase factor.
If f
is integrable, then the Fourier integral is convergent for all w
.
The Fourier integral of an L^1
function is a continuous function.
Fourier theory for functions on π
#
The Fourier transform integral for f : π β E
, with respect to the measure ΞΌ
and additive
character e
.
Equations
- fourier.fourier_integral e ΞΌ f w = vector_fourier.fourier_integral e ΞΌ (linear_map.mul π π) f w
The uniform norm of the Fourier transform of f
is bounded by the LΒΉ
norm of f
.
The Fourier transform converts right-translation into scalar multiplication by a phase factor.
The standard additive character of β
, given by Ξ» x, exp (2 * Ο * x * I)
.
Equations
- real.fourier_char = {to_fun := Ξ» (z : multiplicative β), βexp_map_circle (2 * real.pi * βmultiplicative.to_add z), map_one' := real.fourier_char._proof_1, map_mul' := real.fourier_char._proof_2}
The Fourier integral for f : β β E
, with respect to the standard additive character and
measure on β
.