Cumulative count heat bounds

Abstract

Monotone cumulative geometric counts give all positive time summability and two-sided small-time heat bounds.

Theorem 1.1 (The scalar heat estimate from cumulative counts).

$$\begin{array}{rl}& \forall N:\mathbb{N}\to \mathbb{N},\forall cminus,cplus,lambda,q:\mathbb{R},\\ & \forall m:\mathbb{N}\to \mathbb{N},\forall a,u:\mathbb{N}\to \mathbb{R},\\ & \forall F:\mathbb{R}\to \mathbb{N}\to \mathbb{R},\forall S:\mathbb{R}\to \mathbb{R},\\ & \forall gamma,U,Cminus,Cplus:\mathbb{R},\\ & (\mathrm{Monotone}(N)\wedge N(0)=1\wedge 0<cminus\wedge 0<cplus\wedge 1<lambda\wedge 1<q\\ & \wedge (\forall L:\mathbb{N},(cminus\times lambd{a}^L\le \mathrm{NatCast}(N(L))\wedge \mathrm{NatCast}(N(L))\le cplus\times lambd{a}^L))\\ & \wedge m(0)=1\wedge (\forall k:\mathbb{N},m(k+1)=N(k+1){-}_{\mathbb{N}}N(k))\wedge a(0)=0\wedge (\forall k:\mathbb{N},a(k+1)=q^{k+1})\\ & \wedge gamma=\frac{\log (lambda)}{\log (q)}\wedge (\forall t:\mathbb{R},\forall L:\mathbb{N},F(t,L)=\mathrm{NatCast}(m(L))\times \exp (-t\times a(L)))\\ & \wedge (\forall t:\mathbb{R},S(t)=\sum _{L:\mathbb{N}}^{\prime }F(t,L))\wedge (\forall k:\mathbb{N},u(k)=lambd{a}^{k+1}\times \exp (-q^k))\\ & \wedge U=\sum _{k:\mathbb{N}}^{\prime }u(k)\wedge Cminus=\frac{cminus}{\exp (1)\times lambda}\wedge Cplus=cplus\times (1+U))\\ & \Rightarrow ((0<gamma\wedge 0<Cminus\wedge 0<Cplus)\\ & \wedge (\forall t:\mathbb{R},0<t\Rightarrow \mathrm{Summable}(L:\mathbb{N}\mapsto F(t,L)))\\ & \wedge (\forall t:\mathbb{R},(0<t\wedge t\le 1)\Rightarrow (Cminus\times t^{-gamma}\le S(t)\wedge S(t)\le Cplus\times t^{-gamma}))).\end{array}$$

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

Source. Repository-derived.

Commentary.

Let N: Nat -> Nat be a monotone cumulative count with N(0)=1. Assume positive real constants cminus and cplus and real bases lambda,q greater than one sandwich every N(L) between cminus lambda^L and cplus lambda^L. NatCast denotes the inclusion of natural numbers into the reals.

Define m: Nat -> Nat by m(0)=1 and m(k+1)=N(k+1)-N(k) for every natural k, using natural subtraction (truncated at zero). Define a: Nat -> Real by a(0)=0 and a(k+1)=q^(k+1) for every natural k.

For real t and natural L, define F(t,L)=NatCast(m(L))exp(-ta(L)), and define S(t) as the infinite sum of F(t,L) over all natural L, including L=0. Set gamma=log(lambda)/log(q). For natural k, put u(k)=lambda^(k+1)*exp(-(q^k)); U is the infinite sum of u(k) over all natural k, including k=0. This superexponential tail series converges. Set Cminus=cminus/(exp(1)lambda) and Cplus=cplus(1+U).

For every positive t the scalar series is summable. For 0<t<=1, its sum S(t) lies between Cminust^(-gamma) and Cplust^(-gamma), with the same constants for all such t and with real powers. The proof uses only cumulative counts, so zero increments and plateaus are allowed.

References

• Truth anchor: D5/S3/Analytic/Asymptotics/CumulativeCountHeatBounds.cumulative_count_heat_bounds