mathlib documentation

analysis.fourier.poisson_summation

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:

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.

source
theorem real.fourier_coeff_tsum_comp_add {f : C(ℝ, β„‚)} (hf : βˆ€ (K : topological_space.compacts ℝ), summable (Ξ» (n : β„€), β€–continuous_map.restrict ↑K (f.comp (continuous_map.add_right ↑n))β€–)) (m : β„€) :
fourier_coeff _.lift m = real.fourier_integral ⇑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.

source
theorem real.tsum_eq_tsum_fourier_integral {f : C(ℝ, β„‚)} (h_norm : βˆ€ (K : topological_space.compacts ℝ), summable (Ξ» (n : β„€), β€–continuous_map.restrict ↑K (f.comp (continuous_map.add_right ↑n))β€–)) (h_sum : summable (Ξ» (n : β„€), real.fourier_integral ⇑f ↑n)) :
βˆ‘' (n : β„€), ⇑f ↑n = βˆ‘' (n : β„€), real.fourier_integral ⇑f ↑n

Poisson's summation formula, most general form.

source
theorem is_O_norm_Icc_restrict_at_top {E : Type u_1} [normed_add_comm_group E] {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.

source
theorem is_O_norm_Icc_restrict_at_bot {E : Type u_1} [normed_add_comm_group E] {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
source
theorem is_O_norm_restrict_cocompact {E : Type u_1} [normed_add_comm_group E] (f : C(ℝ, E)) {b : ℝ} (hb : 0 < b) (hf : ⇑f =O[filter.cocompact ℝ] Ξ» (x : ℝ), |x| ^ -b) (K : topological_space.compacts ℝ) :
(Ξ» (x : ℝ), β€–continuous_map.restrict ↑K (f.comp (continuous_map.add_right x))β€–) =O[filter.cocompact ℝ] Ξ» (x : ℝ), |x| ^ -b
source
theorem real.tsum_eq_tsum_fourier_integral_of_rpow_decay_of_summable {f : ℝ β†’ β„‚} (hc : continuous f) {b : ℝ} (hb : 1 < b) (hf : f =O[filter.cocompact ℝ] Ξ» (x : ℝ), |x| ^ -b) (hFf : summable (Ξ» (n : β„€), real.fourier_integral f ↑n)) :
βˆ‘' (n : β„€), f ↑n = βˆ‘' (n : β„€), real.fourier_integral f ↑n

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

source
theorem real.tsum_eq_tsum_fourier_integral_of_rpow_decay {f : ℝ β†’ β„‚} (hc : continuous f) {b : ℝ} (hb : 1 < b) (hf : f =O[filter.cocompact ℝ] Ξ» (x : ℝ), |x| ^ -b) (hFf : real.fourier_integral f =O[filter.cocompact ℝ] Ξ» (x : ℝ), |x| ^ -b) :
βˆ‘' (n : β„€), f ↑n = βˆ‘' (n : β„€), real.fourier_integral f ↑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.)

source
theorem schwartz_map.tsum_eq_tsum_fourier_integral (f g : schwartz_map ℝ β„‚) (hfg : real.fourier_integral ⇑f = ⇑g) :
βˆ‘' (n : β„€), ⇑f ↑n = βˆ‘' (n : β„€), ⇑g ↑n

Poisson's summation formula for Schwartz functions.