A smooth compactly supported function with nonnegative Fourier transform

On a finite-dimensional real inner-product space there is a smooth, compactly supported function psi whose Fourier transform is real and nonnegative everywhere and strictly positive at the origin. Such a test function turns a limit statement about a Fourier-weighted sum with nonnegative summands into an upper bound on the summands near the origin of the frequency variable, which is how Tauberian arguments extract a Chebyshev-type growth bound from smoothed asymptotics.

The function is the autocorrelation g ⋆ g of a real bump function g. The bump function is even and real, so its Fourier transform is real (TauCeti.fourier_eq_re_of_map_neg_eq_conj), and the Fourier transform of the convolution is the square of that real number (Real.fourier_mul_convolution_eq). At the origin it is the square of ∫ g, which is positive.

Main results

• TauCeti.exists_contDiff_hasCompactSupport_fourier_nonneg: a smooth compactly supported function whose Fourier transform is nonnegative everywhere and positive at 0.

theorem TauCeti.exists_contDiff_hasCompactSupport_fourier_nonneg {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] : ∃ (psi : V → ℂ), ContDiff ℝ (↑⊤) psi ∧ HasCompactSupport psi ∧ (∀ (ξ : V), 0 ≤ FourierTransform.fourier psi ξ) ∧ 0 < FourierTransform.fourier psi 0

There is a smooth compactly supported complex-valued function on V whose Fourier transform is nonnegative (in ComplexOrder, so real and nonnegative) at every frequency and strictly positive at the origin.