# mathlib3documentation

analysis.fourier.poisson_summation

# Poisson's summation formula #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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. See real.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.

theorem real.fourier_coeff_tsum_comp_add {f : C(, )} (hf : (K : , summable (λ (n : ), ) (m : ) :

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.

theorem real.tsum_eq_tsum_fourier_integral {f : C(, )} (h_norm : (K : , summable (λ (n : ), ) (h_sum : summable (λ (n : ), ) :
∑' (n : ), f n = ∑' (n : ),

Poisson's summation formula, most general form.

theorem is_O_norm_Icc_restrict_at_top {E : Type u_1} {f : C(, E)} {b : } (hb : 0 < b) (hf : f =O[filter.at_top] λ (x : ), |x| ^ -b) (R S : ) :
(λ (x : ), continuous_map.restrict (set.Icc (x + R) (x + S)) f) =O[filter.at_top] λ (x : ), |x| ^ -b

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.

theorem is_O_norm_Icc_restrict_at_bot {E : Type u_1} {f : C(, E)} {b : } (hb : 0 < b) (hf : f =O[filter.at_bot] λ (x : ), |x| ^ -b) (R S : ) :
(λ (x : ), continuous_map.restrict (set.Icc (x + R) (x + S)) f) =O[filter.at_bot] λ (x : ), |x| ^ -b
theorem is_O_norm_restrict_cocompact {E : Type u_1} (f : C(, E)) {b : } (hb : 0 < b) (hf : f =O[] λ (x : ), |x| ^ -b)  :
(λ (x : ), =O[] λ (x : ), |x| ^ -b
theorem real.tsum_eq_tsum_fourier_integral_of_rpow_decay_of_summable {f : } (hc : continuous f) {b : } (hb : 1 < b) (hf : f =O[] λ (x : ), |x| ^ -b) (hFf : summable (λ (n : ), ) :
∑' (n : ), f n = ∑' (n : ),

Poisson's summation formula, assuming that f decays as |x| ^ (-b) for some 1 < b and its Fourier transform is summable.

theorem real.tsum_eq_tsum_fourier_integral_of_rpow_decay {f : } (hc : continuous f) {b : } (hb : 1 < b) (hf : f =O[] λ (x : ), |x| ^ -b) (hFf : =O[] λ (x : ), |x| ^ -b) :
∑' (n : ), f n = ∑' (n : ),

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.)

theorem schwartz_map.tsum_eq_tsum_fourier_integral (f g : ) (hfg : = g) :
∑' (n : ), f n = ∑' (n : ), g n

Poisson's summation formula for Schwartz functions.