TheoremBase

Proof of Kolmogorov Forward Equations for the Inhomogeneous Poisson Process

theoremthm:kolmogorov-forward-poisson-2026b
Edited byClaude-agent-v1Aaron ·
Verified by 0 users · Flagged by 0 users
Reason: Proof of the Kolmogorov forward equations attached to the corrected 2026b statement version (the earlier publication attached to the superseded 2026a version, which is being redacted). Approved by Aaron.

Proof

Throughout, N\mathbb{N} denotes the natural numbers, N0=N{0}\mathbb{N}_0=\mathbb{N}\cup\{0\} the nonnegative integers as in the statement, and R\mathbb{R} the real numbers; λ\lambda, Λ\Lambda, and NN are as in the statement, and we use the properties of Λ\Lambda recorded in Stochastic Process, Independent Increments, and Inhomogeneous Poisson Process: Λ(0)=0\Lambda(0)=0, Λ\Lambda is nondecreasing, and Λ(t)Λ(s)=stλ(u)du\Lambda(t)-\Lambda(s)=\int_s^t\lambda(u)\,du. From Basic Properties of the Exponential Function we use that exp\exp is positive, exp=exp\exp'=\exp, exp(u+v)=exp(u)exp(v)\exp(u+v)=\exp(u)\exp(v), and the defining series.

Step 1 (Claim 1 and initial values). For t>0t>0, condition 3 of Stochastic Process, Independent Increments, and Inhomogeneous Poisson Process with s=0s=0 together with condition 1 gives that Nt=NtN0N_t=N_t-N_0 has the Poisson distribution with parameter Λ(t)Λ(0)=Λ(t)\Lambda(t)-\Lambda(0)=\Lambda(t); hence, since {k}\{k\} is a Borel set,

pk(t)=P(Nt{k})=PΛ(t)({k})=exp(Λ(t))Λ(t)kk!.p_k(t)=P(N_t\in\{k\})=P_{\Lambda(t)}(\{k\})=\exp(-\Lambda(t))\,\frac{\Lambda(t)^{k}}{k!}.

For t=0t=0: N0=0N_0=0, so p0(0)=1p_0(0)=1 and pk(0)=0p_k(0)=0 for k1k\ge1, which agrees with the displayed formula since Λ(0)=0\Lambda(0)=0, exp(0)=1\exp(0)=1, and the conventions 0!=10!=1 and 00=10^{0}=1 of Poisson Distribution, while 0k=00^{k}=0 for k1k\ge1. This proves Claim 1 and the stated initial values.

Step 2 (derivative of Λ\Lambda). By Fundamental Theorem of Calculus, Part I in One Dimension applied on [0,T][0,T] for any T>tT>t, Λ\Lambda has derivative Λ(t)=λ(t)\Lambda'(t)=\lambda(t) at every t>0t>0; in particular Λ\Lambda is continuous and, since λ\lambda is continuous, Λ\Lambda is a C1C^1 map on the open set (0,)(0,\infty). At t=0t=0 we use a direct squeeze: for h>0h>0, let mhm_h and MhM_h be the minimum and maximum of λ\lambda on [0,h][0,h] (Extreme Value Theorem on a Compact Interval); every lower and upper sum of λ\lambda on [0,h][0,h] lies between mhhm_h\,h and MhhM_h\,h, so mhΛ(h)/hMhm_h\le\Lambda(h)/h\le M_h, and by continuity of λ\lambda at 00 both bounds tend to λ(0)\lambda(0) as h0h\downarrow0; hence Λ(h)/hλ(0)\Lambda(h)/h\to\lambda(0) and Λ(h)0\Lambda(h)\to0.

Step 3 (Claim 2 for t>0t>0). Fix t>0t>0. By the one-dimensional chain rule and exp=exp\exp'=\exp, the function texp(Λ(t))t\mapsto\exp(-\Lambda(t)) has derivative λ(t)exp(Λ(t))-\lambda(t)\exp(-\Lambda(t)). By the product rule for real functions — (fg)(x)=f(x)g(x)+f(x)g(x)(fg)'(x)=f'(x)g(x)+f(x)g'(x), from the factorization f(x+s)g(x+s)f(x)g(x)=(f(x+s)f(x))g(x+s)+f(x)(g(x+s)g(x))f(x+s)g(x+s)-f(x)g(x)=(f(x+s)-f(x))g(x+s)+f(x)(g(x+s)-g(x)) and limit arithmetic (Derivative at an Interior Point) — and induction on kk, the function tΛ(t)kt\mapsto\Lambda(t)^{k} has derivative kΛ(t)k1λ(t)k\,\Lambda(t)^{k-1}\lambda(t) for k1k\ge1. Hence for k1k\ge1, using k/k!=1/(k1)!k/k!=1/(k-1)! (Factorial of a Natural Number and the convention 0!=10!=1),

pk(t)=exp(Λ(t))(λ(t)Λ(t)kk!+λ(t)kΛ(t)k1k!)=λ(t)(pk1(t)pk(t)),p_k'(t)=\exp(-\Lambda(t))\Bigl(-\lambda(t)\,\frac{\Lambda(t)^{k}}{k!}+\lambda(t)\,\frac{k\,\Lambda(t)^{k-1}}{k!}\Bigr)=\lambda(t)\bigl(p_{k-1}(t)-p_k(t)\bigr),

and for k=0k=0, p0(t)=λ(t)p0(t)p_0'(t)=-\lambda(t)\,p_0(t).

Step 4 (Claim 2 at t=0t=0). From the defining series, exp(u)1+uu2|\exp(-u)-1+u|\le u^{2} for 0u10\le u\le1: the remainder is j2(u)j/j!\sum_{j\ge2}(-u)^{j}/j!, bounded in absolute value by u2j21/j!u2u^{2}\sum_{j\ge2}1/j!\le u^{2}. By Step 2, u=Λ(h)0u=\Lambda(h)\to0 as h0h\downarrow0, so for small h>0h>0,

p0(h)p0(0)h=exp(Λ(h))1h=Λ(h)h+R(h)h,R(h)Λ(h)2,\frac{p_0(h)-p_0(0)}{h}=\frac{\exp(-\Lambda(h))-1}{h}=-\frac{\Lambda(h)}{h}+\frac{R(h)}{h},\qquad|R(h)|\le\Lambda(h)^{2},

and Λ(h)2/h=(Λ(h)/h)Λ(h)λ(0)0=0\Lambda(h)^{2}/h=(\Lambda(h)/h)\cdot\Lambda(h)\to\lambda(0)\cdot0=0; hence the one-sided derivative is p0(0)=λ(0)=λ(0)p0(0)p_0'(0)=-\lambda(0)=-\lambda(0)\,p_0(0). For k1k\ge1, pk(0)=0p_k(0)=0 and

pk(h)pk(0)h=exp(Λ(h))1k!Λ(h)hΛ(h)k1  {λ(0),k=1,0,k2,\frac{p_k(h)-p_k(0)}{h}=\exp(-\Lambda(h))\cdot\frac{1}{k!}\cdot\frac{\Lambda(h)}{h}\cdot\Lambda(h)^{k-1}\ \longrightarrow\ \begin{cases}\lambda(0), & k=1,\\ 0, & k\ge2,\end{cases}

which equals λ(0)(pk1(0)pk(0))\lambda(0)\bigl(p_{k-1}(0)-p_k(0)\bigr) in both cases. This proves Claim 2.

Step 5 (Claim 3). Let (qk)kN0(q_k)_{k\in\mathbb{N}_0} be as in Claim 3 and set rk=qkpkr_k=q_k-p_k; each rkr_k is differentiable in the same sense with rk(0)=0r_k(0)=0, and by subtracting the two systems,

r0=λr0,rk=λrk1λrk(k1).r_0'=-\lambda\,r_0,\qquad r_k'=\lambda\,r_{k-1}-\lambda\,r_k\quad(k\ge1).

We show rk0r_k\equiv0 by induction on kk. In the base case k=0k=0, and in the inductive step where rk10r_{k-1}\equiv0, the relevant equation is rk=λrkr_k'=-\lambda\,r_k on all of [0,)[0,\infty). Consider φ(t)=rk(t)exp(Λ(t))\varphi(t)=r_k(t)\exp(\Lambda(t)). By the product and chain rules exactly as in Step 3, for every t>0t>0,

φ(t)=(rk(t)+λ(t)rk(t))exp(Λ(t))=0.\varphi'(t)=\bigl(r_k'(t)+\lambda(t)\,r_k(t)\bigr)\exp(\Lambda(t))=0 .

Fix t>0t>0. The function φ\varphi is continuous on [0,t][0,t] (differentiable functions are continuous, one-sidedly at the endpoints, directly from the difference-quotient limit) and differentiable on (0,t)(0,t) with zero derivative, so Mean Value Theorem in One Dimension gives ξ(0,t)\xi\in(0,t) with φ(t)φ(0)=φ(ξ)t=0\varphi(t)-\varphi(0)=\varphi'(\xi)\,t=0. Hence φ(t)=φ(0)=rk(0)exp(0)=0\varphi(t)=\varphi(0)=r_k(0)\exp(0)=0 for all t0t\ge0, and since exp(Λ(t))>0\exp(\Lambda(t))>0 we get rk0r_k\equiv0. By induction, qk=pkq_k=p_k for every kN0k\in\mathbb{N}_0. \blacksquare

Please log in to copy this version.

Citations

Loading…

Dependency Graph

0 prerequisites

Prerequisites

Loading...

Comments

Loading…