English
The m-th Fourier coefficient of a periodic Poisson-summed function equals the Fourier transform evaluated at m, under suitable summability hypotheses.
Русский
m-я фурье-коэффициента периодической функции, полученной суммированием по Пуассону, равна значению Фурье-преобразования в m, при подходящих предположениях суммируемости.
LaTeX
$$$$ \widehat{f}_{ ext{periodic}}(m) = \mathcal{F} f(m) $$$$
Lean4
/-- 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 fourierCoeff_tsum_comp_add {f : C(ℝ, ℂ)}
(hf : ∀ K : Compacts ℝ, Summable fun n : ℤ => ‖(f.comp (ContinuousMap.addRight n)).restrict K‖) (m : ℤ) :
fourierCoeff (Periodic.lift <| f.periodic_tsum_comp_add_zsmul 1) m = 𝓕 f m := by
-- NB: This proof can be shortened somewhat by telescoping together some of the steps in the calc
-- block, but I think it's more legible this way. We start with preliminaries about the integrand.
let e : C(ℝ, ℂ) := (fourier (-m)).comp ⟨((↑) : ℝ → UnitAddCircle), continuous_quotient_mk'⟩
have neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖(e * g).restrict K‖ = ‖g.restrict K‖ :=
by
have (x : ℝ) : ‖e x‖ = 1 := (AddCircle.toCircle (-m • x)).norm_coe
intro K g
simp_rw [norm_eq_iSup_norm, restrict_apply, mul_apply, norm_mul, this, one_mul]
have eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight n) = e :=
by
intro n; ext1 x
have : Periodic e 1 := Periodic.comp (fun x => AddCircle.coe_add_period 1 x) (fourier (-m))
simpa only [mul_one] using this.int_mul n x
calc
fourierCoeff (Periodic.lift <| f.periodic_tsum_comp_add_zsmul 1) m =
∫ x in (0 : ℝ)..1, e x * (∑' n : ℤ, f.comp (ContinuousMap.addRight n)) x :=
by
simp_rw [fourierCoeff_eq_intervalIntegral _ m 0, div_one, one_smul, zero_add, e, comp_apply, coe_mk,
Periodic.lift_coe, zsmul_one, smul_eq_mul]
-- Transform sum in C(ℝ, ℂ) evaluated at x into pointwise sum of values.
_ = ∫ x in (0 : ℝ)..1, ∑' n : ℤ, (e * f.comp (ContinuousMap.addRight n)) x := by
simp_rw [coe_mul, Pi.mul_apply, ← ContinuousMap.tsum_apply (summable_of_locally_summable_norm hf), tsum_mul_left]
-- Swap sum and integral.
_ = ∑' n : ℤ, ∫ x in (0 : ℝ)..1, (e * f.comp (ContinuousMap.addRight n)) x :=
by
refine (intervalIntegral.tsum_intervalIntegral_eq_of_summable_norm ?_).symm
convert hf ⟨uIcc 0 1, isCompact_uIcc⟩ using 1
exact funext fun n => neK _ _
_ = ∑' n : ℤ, ∫ x in (0 : ℝ)..1, (e * f).comp (ContinuousMap.addRight n) x :=
by
simp only [mul_comp] at eadd ⊢
simp_rw [eadd]
-- Rearrange sum of interval integrals into an integral over `ℝ`.
_ = ∫ x, e x * f x :=
by
suffices Integrable (e * f) from this.hasSum_intervalIntegral_comp_add_int.tsum_eq
apply integrable_of_summable_norm_Icc
convert hf ⟨Icc 0 1, isCompact_Icc⟩ using 1
simp_rw [mul_comp] at eadd ⊢
simp_rw [eadd]
exact
funext fun n =>
neK ⟨Icc 0 1, isCompact_Icc⟩
_
-- Minor tidying to finish
_ = 𝓕 f m := by
rw [fourierIntegral_real_eq_integral_exp_smul]
congr 1 with x : 1
rw [smul_eq_mul, comp_apply, coe_mk, coe_mk, ContinuousMap.toFun_eq_coe, fourier_coe_apply]
congr 2
push_cast
ring
