Finite Counterterm Mellin Continuation

Abstract

Finite local counterterms give a meromorphic Mellin continuation.

Theorem 1.1 (Finite counterterms continue the Mellin transform).

$$\begin{array}{r}\forall m:\mathbb{N},\theta :\mathbb{R}\to \mathbb{C},a:\mathrm{Fin}(m)\to \mathbb{C},\\ \alpha :\mathrm{Fin}(m+1)\to \mathbb{R},\Delta :\mathbb{R};\\ letR:\mathbb{R}\to \mathbb{C},R(t)=\theta (t)-\sum _{j:\mathrm{Fin}(m)}a(j)(t:\mathbb{C}{)}^{-\alpha (j)};\\ let{\theta }_{reg}:\mathbb{R}\to \mathbb{C},{\theta }_{reg}(t)=ift\le 1thenR(t)else\theta (t);\\ let{M}_m:\mathbb{C}\to \mathbb{C},M_m(s)=\mathrm{setIntegral}(\mathrm{Ioc}(0,1),(t:\mathbb{C}{)}^{s-1}R(t))+\mathrm{setIntegral}(\mathrm{Ioi}(1),(t:\mathbb{C}{)}^{s-1}\theta (t))+\sum _{j:\mathrm{Fin}(m)}\frac{a(j)}{s-\alpha (j)};\\ \mathrm{StrictAnti}(\alpha )\wedge 0<\Delta \wedge \\ \mathrm{LocallyIntegrableOn}({\theta }_{reg},\mathrm{Ioi}(0))\wedge \\ \mathrm{IsBigO}(nhdsWithin(0,\mathrm{Ioi}(0)),R,t\mapsto t^{-\alpha (last(m))})\wedge \\ \mathrm{IsBigO}(atTop,\theta ,t\mapsto exp(-\Delta t))\Rightarrow \\ \mathrm{MeromorphicOn}(M_m,\{s\in \mathbb{C}:\alpha (last(m))<\Re (s)\})\wedge \\ \forall s:\mathbb{C},\alpha (0)<\Re (s)\Rightarrow \mathrm{MellinConvergent}(\theta ,s)\wedge M_m(s)=\mathrm{mellin}(\theta ,s).\end{array}$$

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

Source. Repository-derived.

Commentary.

Let theta be a complex-valued heat trace, let a be a finite family of local coefficients, and let alpha be a strictly decreasing list of real exponents with one additional residual exponent. The displayed regularized trace is constructed by subtracting the finite principal part only on the interval ending at one.

The hypotheses state local integrability of that exact piecewise trace, the residual power bound at zero, and exponential decay of theta at infinity. These analytic assumptions are all explicit in the Lean signature; none is hidden in a named source object.

The continued function is the literal sum of the two split integrals and the finite rational pole ledger. It is meromorphic on the half-plane to the right of the residual exponent, and on the original convergence half-plane theta has a convergent Mellin transform equal to this continuation.

Repository search found no theorem with this general finite-counterterm carrier. The proof applies Mathlib’s Mellin convergence and differentiability theorem for simultaneous power and exponential bounds, the exact Mellin transform of a power on (0,1], and the standard closure rules for finite sums of meromorphic functions.

References

• Truth anchor: D5/S3/Analytic/Asymptotics/FiniteCountertermMellinContinuation.finite_counterterm_mellin_continuation