Poisson's summation formula #
We prove Poisson's summation formula β (n : β€), f n = β (n : β€), π f n
, where π f
is the
Fourier transform of f
, under the following hypotheses:
f
is a continuous functionβ β β
.- The sum
β (n : β€), π f n
is convergent. - For all compacts
K β β
, the sumβ (n : β€), sup { βf(x + n)β | x β K }
is convergent. Seereal.tsum_eq_tsum_fourier_integral
for this formulation.
These hypotheses are potentially a little awkward to apply, so we also provide the less general but
easier-to-use result real.tsum_eq_tsum_fourier_integral_of_rpow_decay
, in which we assume f
and
π f
both decay as |x| ^ (-b)
for some b > 1
, and the even more specific result
schwartz_map.tsum_eq_tsum_fourier_integral
, where we assume that both f
and π f
are Schwartz
functions.
TODO #
At the moment schwartz_map.tsum_eq_tsum_fourier_integral
requires separate proofs that both f
and π f
are Schwartz functions. In fact, π f
is automatically Schwartz if f
is; and once
we have this lemma in the library, we should adjust the hypotheses here accordingly.
The key lemma for Poisson summation: the m
-th Fourier coefficient of the periodic function
β' n : β€, f (x + n)
is the value at m
of the Fourier transform of f
.
Poisson's summation formula, most general form.
If f
is O(x ^ (-b))
at infinity, then so is the function
Ξ» x, βf.restrict (Icc (x + R) (x + S))β
for any fixed R
and S
.
Poisson's summation formula, assuming that f
decays as
|x| ^ (-b)
for some 1 < b
and its Fourier transform is summable.
Poisson's summation formula, assuming that both f
and its Fourier transform decay as
|x| ^ (-b)
for some 1 < b
. (This is the one-dimensional case of Corollary VII.2.6 of Stein and
Weiss, Introduction to Fourier analysis on Euclidean spaces.)