English
The Fourier integral can be rewritten via a half-period translation formula, expressing the original integral as a half of a translated difference of f and f shifted by i w, enabling uniform-continuity arguments.
Русский
Преобразование Фурье можно переписать через формулу полупериодного переноса, выражая исходный интеграл через половину разности f и f(·+i w).
LaTeX
$$$\\int_V e^{-⟨v,w⟩} f(v) dv = \\tfrac{1}{2}\\int_V e^{-⟨v,w⟩} (f(v) - f(v+i w)) dv$$$
Lean4
/-- Rewrite the Fourier integral in a form that allows us to use uniform continuity. -/
theorem fourierIntegral_eq_half_sub_half_period_translate {w : V} (hw : w ≠ 0) (hf : Integrable f) :
∫ v : V, 𝐞 (-⟪v, w⟫) • f v = (1 / (2 : ℂ)) • ∫ v : V, 𝐞 (-⟪v, w⟫) • (f v - f (v + i w)) :=
by
simp_rw [smul_sub]
rw [integral_sub, fourierIntegral_half_period_translate hw, sub_eq_add_neg, neg_neg, ← two_smul ℂ _, ←
@smul_assoc _ _ _ _ _ _ (IsScalarTower.left ℂ), smul_eq_mul]
· simp
exacts [(Real.fourierIntegral_convergent_iff w).2 hf, (Real.fourierIntegral_convergent_iff w).2 (hf.comp_add_right _)]
