Spectral Zeta Continuation With Convergence

Abstract

Linear spectral density yields a convergent spectral series and its meromorphic continuation.

Theorem 1.1 (Linear density gives convergence, continuation, and residue).

$$\begin{array}{r}\forall \lambda :\mathbb{N}\to \mathbb{R},c:\mathbb{R};\\ \left(Z_{\lambda }\right)\left(s\right):=\sum _{n:\mathbb{N}}(\lambda \left(n\right):\mathbb{C}{)}^{-s};\\ \left(N_{\lambda }\right)\left(u\right):=\mathrm{card}(\{n\in \mathbb{N}\mid \lambda \left(n\right)\le u\});\\ \left(Z{c}_{\lambda }\right)\left(s\right):=\mathrm{continuedSpectralZeta}(\lambda ,c,s);\\ (\forall n:\mathbb{N},0<\lambda \left(n\right))\wedge \mathrm{StrictMono}(\lambda )\wedge \\ (\forall u:\mathbb{R},\mathrm{Finite}(\{n\in \mathbb{N}\mid \lambda \left(n\right)\le u\}))\wedge \mathrm{IsBigO}(atTop,u\mapsto \left(N_{\lambda }\right)\left(u\right)-cu,u\mapsto 1)\Rightarrow \\ (\mathrm{MeromorphicOn}(Z{c}_{\lambda },\{s\in \mathbb{C}\mid 0<\Re (s)\})\wedge \forall s:\mathbb{C},1<\Re (s)\Rightarrow \left(Z{c}_{\lambda }\right)\left(s\right)=\left(Z_{\lambda }\right)\left(s\right))\wedge \\ (\forall s:\mathbb{C},1<\Re (s)\Rightarrow \mathrm{Summable}((n:\mathbb{N})\mapsto (\lambda \left(n\right):\mathbb{C}{)}^{-s}))\wedge \\ \mathrm{Tendsto}((s:\mathbb{C})\mapsto (s-1)\left(Z{c}_{\lambda }\right)\left(s\right),\mathrm{nhdsWithin}(1,\mathbb{C}\setminus \{1\}),\mathrm{nhds}((c:\mathbb{C}))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Asymptotics/SpectralZetaContinuationConvergence.linear_density_spectral_zeta_continuation_with_convergence (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let lambda be a positive strictly increasing real spectrum with finite sublevel sets. Its counting function N_lambda(u) counts the indices whose spectral value is at most u, and the density hypothesis is N_lambda(u)-c u=O(1) at infinity.

The named continued spectral zeta function is meromorphic on Re(s)>0 and agrees with the displayed spectral Dirichlet series on Re(s)>1. The statement separately exposes summability of the exact complex terms lambda(n)^(-s) throughout that initial half-plane, so the displayed series is not merely a totalized infinite sum.

The continuation also has residue c at s=1, expressed as the exact punctured-neighborhood limit of (s-1) times the continuation. The proof reuses the frozen continuation, residue, and convergence declarations without duplicating their proof bodies.

References

• Truth anchor: D5/S3/Analytic/Asymptotics/SpectralZetaContinuationConvergence.linear_density_spectral_zeta_continuation_with_convergence
• Dependency: D5/S3/Analytic/Asymptotics/SpectralZetaContinuation