Convolution-Square Positivity
Abstract
The Fourier transform of a Weil convolution square is a nonnegative real norm square.
Theorem 1.1 (Angular frequency matches mathlib Fourier frequency).
Proof. Machine-checked in Lean as D5/S3/Weil/TestFunctions/ConvolutionSquarePositivity.fourierLaplace_real_eq_fourier (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every Weil test function, the angular-frequency Fourier-Laplace transform at xi equals mathlib’s real Fourier transform at xi divided by two pi. The theorem is the normalization bridge between the repository kernel and mathlib’s Fourier convention.
Theorem 1.2 (A convolution square transforms to a norm square).
Proof. Machine-checked in Lean as D5/S3/Weil/TestFunctions/ConvolutionSquarePositivity.fourierLaplace_convolutionSquare_real (✓ std3). ∎
Source. Repository-derived.
Commentary.
The real-axis transform of g convolved with its Weil involution is the complex norm square of the transform of g. The proof applies mathlib’s Fourier convolution theorem and converts the involution transform to complex conjugation.
Theorem 1.3 (A convolution-square transform is real and nonnegative).
Proof. Machine-checked in Lean as D5/S3/Weil/TestFunctions/ConvolutionSquarePositivity.fourierLaplace_convolutionSquare_real_nonnegative (✓ std3). ∎
Source. Repository-derived.
Commentary.
Because the preceding identity is a real norm square, its imaginary part vanishes and its real part is nonnegative at every real frequency. This is the Fourier-side positivity kernel for convolution-square Weil tests.
References
- Truth anchor:
D5/S3/Weil/TestFunctions/ConvolutionSquarePositivity.fourierLaplace_convolutionSquare_real - Truth anchor:
D5/S3/Weil/TestFunctions/ConvolutionSquarePositivity.fourierLaplace_convolutionSquare_real_nonnegative - Truth anchor:
D5/S3/Weil/TestFunctions/ConvolutionSquarePositivity.fourierLaplace_real_eq_fourier