Integrability of Fourier transforms of smooth compactly supported functions #
A smooth compactly supported function is a Schwartz function, so its Fourier transform is also a Schwartz function and hence integrable. This supplies the Fourier-integrability hypotheses needed in dominated-convergence arguments, such as the Wiener--Ikehara boundary identity.
Main declarations #
TauCeti.integrable_fourier_of_contDiff_of_hasCompactSupport: the Fourier transform of a smooth compactly supported function on a finite-dimensional real inner product space is integrable.
theorem
TauCeti.integrable_fourier_of_contDiff_of_hasCompactSupport
{V : Type u_1}
{E : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{f : V → E}
(hf : ContDiff ℝ (↑⊤) f)
(hsupp : HasCompactSupport f)
:
The Fourier transform of a smooth compactly supported function is integrable.