Infinite Sinc Product

Abstract

Dyadic uniform-interval Fourier factors form a sinc product nonzero off the real axis.

Theorem 1.1 (The dyadic sinc product is nonzero away from the real axis).

$$\forall ell\in \mathrm{Real}\left(\right),0<ell\Rightarrow \left(\left(\left(\left(\forall n\in \mathrm{Natural}\left(\right),\left(\left(\left(\left(0<\mathrm{dyadicHalfWidth}\left(ell,n\right)\wedge \left(\forall x\in \mathrm{Real}\left(\right),0\le \mathrm{uniformIntervalDensity}\left(\mathrm{dyadicHalfWidth}\left(ell,n\right),x\right)\right)\right)\wedge \left(\forall x\in \mathrm{Real}\left(\right),\mathrm{uniformIntervalDensity}\left(\mathrm{dyadicHalfWidth}\left(ell,n\right),-x\right)=\mathrm{uniformIntervalDensity}\left(\mathrm{dyadicHalfWidth}\left(ell,n\right),x\right)\right)\right)\wedge \mathrm{Integrable}\left(\mathrm{uniformIntervalDensity}\left(\mathrm{dyadicHalfWidth}\left(ell,n\right)\right)\right)\right)\wedge \mathrm{integral}\left(\mathrm{uniformIntervalDensity}\left(\mathrm{dyadicHalfWidth}\left(ell,n\right)\right)\right)=1\right)\wedge \left(\forall z\in \mathrm{Complex}\left(\right),\mathrm{uniformIntervalFourierLaplace}\left(\mathrm{dyadicHalfWidth}\left(ell,n\right),z\right)=\mathrm{complexSinc}\left(\mathrm{dyadicHalfWidth}\left(ell,n\right)\cdot z\right)\right)\right)\wedge \mathrm{tsum}\left({\left(\mathrm{dyadicHalfWidth}\left(ell,n\right)\right)}_{n\in \mathrm{Natural}\left(\right)}\right)=\frac{ell}{2}\right)\wedge \left(\forall K\in \mathrm{Set}\left(\mathrm{Complex}\left(\right)\right),\mathrm{IsCompact}\left(K\right)\Rightarrow \mathrm{HasProdUniformlyOn}\left((n:\mathrm{Natural}\left(\right),z:\mathrm{Complex}\left(\right)\mapsto \mathrm{complexSinc}\left(\mathrm{dyadicHalfWidth}\left(ell,n\right)\cdot z\right)),(z:\mathrm{Complex}\left(\right)\mapsto \mathrm{tprod}\left({\left(\mathrm{complexSinc}\left(\mathrm{dyadicHalfWidth}\left(ell,n\right)\cdot z\right)\right)}_{n\in \mathrm{Natural}\left(\right)}\right)),K\right)\right)\right)\wedge \left(\forall z\in \mathrm{Complex}\left(\right),\mathrm{im}\left(z\right)\ne 0\Rightarrow \mathrm{tprod}\left({\left(\mathrm{complexSinc}\left(\mathrm{dyadicHalfWidth}\left(ell,n\right)\cdot z\right)\right)}_{n\in \mathrm{Natural}\left(\right)}\right)\ne 0\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Fourier/InfiniteSincProduct.dyadic_uniform_convolution_product_ne_zero_off_real (✓ std3). ∎

Source. Repository-derived.

Commentary.

For positive ell, the nth half-width is ell divided by 2^(n+2). Each associated uniform interval density is nonnegative, even, integrable, and has integral one. Its complex Fourier-Laplace transform is the corresponding removable sinc factor.

The half-widths sum to ell/2 and their squares are summable. A quadratic estimate for complex sinc minus one gives uniform convergence of the product on every compact subset of the complex plane.

Every factor is nonzero at a point with nonzero imaginary part. Absolute summability of the factor deviations then prevents the infinite product itself from vanishing there.

This theorem records the interval components, their exact transform factors, and the infinite-product conclusion. It does not construct the limiting convolution density or assert smoothness and decay.

References

• Truth anchor: D5/S3/Fourier/InfiniteSincProduct.dyadic_uniform_convolution_product_ne_zero_off_real