PrimeNumberTheoremAnd

The exponentially damped sinc function is integrable on the positive half-line.

Uniform half-line tail control for the damped one-sided sinc integral.

On a fixed finite window, damping tends back to the undamped sinc integral.

Abel comparison: any finite-window sinc limit agrees with the damped half-line limit.

Evaluation of the damped sinc integral from the one remaining Fubini swap. The hypothesis is the exact product-integrability/swap term left to prove.

Product-integrability of the damped sine kernel on (0,∞) × (a,∞). The proof integrates the u-tail first and bounds the inner norm by exp (-a*x) using |sin x| ≤ x for x > 0.

Abel limit of the Laplace-regularized sinc integral as the damping tends to zero from the right.

The scalar finite-window sine-kernel mass is eventually bounded by 2.

Windowed principal-value convergence for the sinc kernel. This avoids treating the non-integrable constant kernel mass as a whole-line Bochner integral: the remaining analytic work is split into a finite-window mass limit, a finite-window local error limit, and a tail-control limit.

Windowed principal-value convergence with the finite-window mass discharged by the scalar sinc limit.

Windowed principal-value convergence from local quotient integrability and tail control.

Principal-value Laplace inversion reduced to the corresponding truncated Fourier convergence theorem for the exponentially weighted source.

The truncated multiplication-form inverse Laplace integral is the truncated vector-valued inverse Laplace line integral at log x.

Principal-value Laplace inversion in the multiplication x^s form, reduced to truncated Fourier convergence for the exponentially weighted source.

A continuous function that decays like a negative exponential at +∞ and is controlled by a positive exponential at -∞ is globally bounded.

Continuity of the bilateral Laplace integral along the σ + tI vertical line, under integrability of the exponentially weighted source. Companion to continuous_laplaceIntegral_verticalLine_of_integrable (the σ - tI form).

A family of constant functions f (i, x) = C i is uniformly bounded w.r.t. s by ⨆ i ∈ s, ‖C i‖, if s is compact and C is continuous.

A family of constant functions f (i, x) = C i is uniformly bounded below w.r.t. s by ⊓ i ∈ s, ‖C i‖, if s is compact and C is continuous.

The logarithmic derivative of the exponential of a complex polynomial is the polynomial derivative.