Finite Paley-Wiener Interpolation

Abstract

Finite conjugation-compatible data admit an exact compact smooth Hermitian Fourier-Laplace interpolant.

Theorem 1.1 (Finite exact Paley-Wiener interpolation).

$$\forall M\in \mathrm{Natural}\left(\right),z\in \mathrm{Fin}\left(M\right)\to \mathrm{Complex}\left(\right),r\in \mathrm{Fin}\left(M\right)\to \mathrm{Complex}\left(\right),conjIndex\in \mathrm{Fin}\left(M\right)\to \mathrm{Fin}\left(M\right),\left(\left(\mathrm{Injective}\left(z\right)\wedge \left(\forall j\in \mathrm{Fin}\left(M\right),z\left(conjIndex\left(j\right)\right)=\mathrm{conj}\left(z\left(j\right)\right)\right)\right)\wedge \left(\forall j\in \mathrm{Fin}\left(M\right),r\left(conjIndex\left(j\right)\right)=\mathrm{conj}\left(r\left(j\right)\right)\right)\right)\Rightarrow \left(\exists L\in \mathrm{Real}\left(\right),psi\in \mathrm{Real}\left(\right)\to \mathrm{Complex}\left(\right),P\in \mathrm{Polynomial}\left(\mathrm{Complex}\left(\right)\right),f\in \mathrm{Real}\left(\right)\to \mathrm{Complex}\left(\right),\left(\left(\left(\left(\left(\left(\left(\left(\left(\left(\left(0<L\wedge \mathrm{ContDiff}\left(\mathrm{Real}\left(\right),\mathrm{infinity}\left(\right),psi\right)\right)\wedge \mathrm{HasCompactSupport}\left(psi\right)\right)\wedge \mathrm{tsupport}\left(psi\right)\subseteq \mathrm{Ioo}\left(-L,L\right)\right)\wedge \left(\forall j\in \mathrm{Fin}\left(M\right),\mathrm{fourierLaplace}\left(psi,z\left(j\right)\right)\ne 0\right)\right)\wedge \left(\forall j\in \mathrm{Fin}\left(M\right),\mathrm{eval}\left(P,z\left(j\right)\right)=\frac{r\left(j\right)}{\mathrm{fourierLaplace}\left(psi,z\left(j\right)\right)}\right)\right)\wedge f=(x:\mathrm{Real}\left(\right)\mapsto \mathrm{sum}\left(k,\mathrm{support}\left(P\right),\mathrm{coeff}\left(P,k\right)\cdot \mathrm{pow}\left(-I\left(\right),k\right)\cdot \mathrm{iterate}\left(deriv,k,psi\right)\left(x\right)\right))\right)\wedge \mathrm{ContDiff}\left(\mathrm{Real}\left(\right),\mathrm{infinity}\left(\right),f\right)\right)\wedge \mathrm{HasCompactSupport}\left(f\right)\right)\wedge \mathrm{tsupport}\left(f\right)\subseteq \mathrm{Ioo}\left(-L,L\right)\right)\wedge \left(\forall x\in \mathrm{Real}\left(\right),f\left(-x\right)=\mathrm{conj}\left(f\left(x\right)\right)\right)\right)\wedge \left(\forall w\in \mathrm{Complex}\left(\right),\mathrm{fourierLaplace}\left(f,w\right)=\mathrm{eval}\left(P,w\right)\cdot \mathrm{fourierLaplace}\left(psi,w\right)\right)\right)\wedge \left(\forall j\in \mathrm{Fin}\left(M\right),\mathrm{fourierLaplace}\left(f,z\left(j\right)\right)=r\left(j\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/TestFunctions/FinitePaleyWienerInterpolation.finite_exact_paley_wiener_interpolation (✓ std3). ∎

Source. Repository-derived.

Commentary.

A normalized compact bump is dilated until its Fourier-Laplace transform is nonzero at every prescribed node. Lagrange interpolation then constructs the polynomial differential multiplier, and integration by parts proves its public transform factorization.

Under the source’s frozen exp(-i z x) convention, integration by parts sends partial_x to i z, so its printed P(i partial_x) psi yields P(-z); the public witness uses P(-i partial_x) to realize the stated P(z) factorization.

Conjugation-compatible nodes and values make the coefficientwise conjugation average of the Lagrange polynomial coefficient-real. Applied to the Hermitian seed, its polynomial differential construction is itself Hermitian, so the same final test function has the differential definition and global transform factorization.

References

• Truth anchor: D5/S3/Weil/TestFunctions/FinitePaleyWienerInterpolation.finite_exact_paley_wiener_interpolation