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. See Real.tsum_eq_tsum_fourierIntegral 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_fourierIntegral_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 SchwartzMap.tsum_eq_tsum_fourierIntegral, where we assume that both f and 𝓕 f are Schwartz functions.

TODO

At the moment SchwartzMap.tsum_eq_tsum_fourierIntegral 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.fourierCoeff_tsum_comp_add {f : C(ℝ, ℂ)} (hf : ∀ (K : TopologicalSpace.Compacts ℝ), Summable fun (n : ℤ) => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖) (m : ℤ) : fourierCoeff (Function.Periodic.lift (_ : Function.Periodic (⇑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1)) m = Real.fourierIntegral ⇑f ↑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_fourierIntegral {f : C(ℝ, ℂ)} (h_norm : ∀ (K : TopologicalSpace.Compacts ℝ), Summable fun (n : ℤ) => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖) (h_sum : Summable fun (n : ℤ) => Real.fourierIntegral ⇑f ↑n) (x : ℝ) : ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), Real.fourierIntegral ⇑f ↑n * (fourier n) ↑x

Poisson's summation formula, most general form.

theorem isBigO_norm_Icc_restrict_atTop {E : Type u_1} [NormedAddCommGroup E] {f : C(ℝ, E)} {b : ℝ} (hb : 0 < b) (hf : ⇑f =O[Filter.atTop] fun (x : ℝ) => |x| ^ (-b)) (R : ℝ) (S : ℝ) : (fun (x : ℝ) => ‖ContinuousMap.restrict (Set.Icc (x + R) (x + S)) f‖) =O[Filter.atTop] fun (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 isBigO_norm_Icc_restrict_atBot {E : Type u_1} [NormedAddCommGroup E] {f : C(ℝ, E)} {b : ℝ} (hb : 0 < b) (hf : ⇑f =O[Filter.atBot] fun (x : ℝ) => |x| ^ (-b)) (R : ℝ) (S : ℝ) : (fun (x : ℝ) => ‖ContinuousMap.restrict (Set.Icc (x + R) (x + S)) f‖) =O[Filter.atBot] fun (x : ℝ) => |x| ^ (-b)

theorem isBigO_norm_restrict_cocompact {E : Type u_1} [NormedAddCommGroup E] (f : C(ℝ, E)) {b : ℝ} (hb : 0 < b) (hf : ⇑f =O[Filter.cocompact ℝ] fun (x : ℝ) => |x| ^ (-b)) (K : TopologicalSpace.Compacts ℝ) : (fun (x : ℝ) => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖) =O[Filter.cocompact ℝ] fun (x : ℝ) => |x| ^ (-b)

theorem Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay_of_summable {f : ℝ → ℂ} (hc : Continuous f) {b : ℝ} (hb : 1 < b) (hf : f =O[Filter.cocompact ℝ] fun (x : ℝ) => |x| ^ (-b)) (hFf : Summable fun (n : ℤ) => Real.fourierIntegral f ↑n) (x : ℝ) : ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), Real.fourierIntegral f ↑n * (fourier n) ↑x

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_fourierIntegral_of_rpow_decay {f : ℝ → ℂ} (hc : Continuous f) {b : ℝ} (hb : 1 < b) (hf : f =O[Filter.cocompact ℝ] fun (x : ℝ) => |x| ^ (-b)) (hFf : Real.fourierIntegral f =O[Filter.cocompact ℝ] fun (x : ℝ) => |x| ^ (-b)) (x : ℝ) : ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), Real.fourierIntegral f ↑n * (fourier n) ↑x

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 SchwartzMap.tsum_eq_tsum_fourierIntegral (f : SchwartzMap ℝ ℂ) (g : SchwartzMap ℝ ℂ) (hfg : Real.fourierIntegral ⇑f = ⇑g) (x : ℝ) : ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), g ↑n * (fourier n) ↑x

Poisson's summation formula for Schwartz functions.