Fourier transform of L¹ positive-definite functions is nonneg

We prove: for φ : V → ℂ continuous, integrable, and positive-definite on a finite-dimensional real inner product space V, Re(𝓕φ(ξ)) ≥ 0 for all ξ.

Proof strategy

For fixed ξ, note that ψ(x) = φ(x) · exp(-2πi⟨x,ξ⟩) is PD (Schur product of φ and the PD function exp(2πi⟨·,-ξ⟩)), continuous, and integrable with 𝓕φ(ξ) = ∫ ψ. So it suffices to show Re(∫ ψ) ≥ 0 for any PD continuous L¹ ψ.

For R > 0, define J_R = (1/μ(B_R)) ∫∫_{B_R × B_R} ψ(x-y) dx dy.

Step A: Re(J_R) ≥ 0 because the double integral is approximated by PD double sums (Riemann sums on V × V with PD structure).

Step B: By Fubini, J_R = ∫ ψ(v) · [μ(B_R ∩ (v+B_R))/μ(B_R)] dv. The kernel → 1 pointwise and is bounded by 1, so DCT gives J_R → ∫ ψ.

Step C: ge_of_tendsto' gives Re(∫ ψ) ≥ 0.

References

• Rudin, Fourier Analysis on Groups, Theorem 1.4.3
• Folland, A Course in Abstract Harmonic Analysis, §4.2, Lemma 4.8

Helper: exp(2πi⟨·,ξ⟩) is positive definite

Haar measure neg-invariance

instance volumeIsNegInvariant {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] : MeasureTheory.volume.IsNegInvariant

Volume on a finite-dimensional inner product space is neg-invariant. Proof: negation is a linear isometry equiv, which preserves addHaar measure.

Step A: The PD double integral has nonneg real part

Integral of PD function has nonneg real part

Step B + C: The main theorem

theorem pd_l1_fourier_re_nonneg_theorem {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (φ : V → ℂ) (hpd : IsPositiveDefinite φ) (hint : MeasureTheory.Integrable φ MeasureTheory.volume) (hcont : Continuous φ) (ξ : V) : 0 ≤ (FourierTransform.fourier φ ξ).re

The Fourier transform of a continuous integrable positive-definite function on a finite-dimensional real inner product space has nonneg real part.