Existence of a locally finite Poisson point process

Put $K_0=\mathrm{\varnothing }$, $A_1=K_1$, and $A_i=K_i\setminus K_{i-1}$ for $i\ge 2$. By [F6], each $K_i$ is closed, so the disjoint sets $A_i$ are Borel and cover $S$. Since $A_i\subseteq K_i$, countable additivity of the measure gives $\nu (A_i)\le \nu (K_i)<\mathrm{\infty }$, hence ${\nu }_i(B):=\nu (B\cap A_i)$ is finite. If $i>m$, then $A_i\cap K_m=\mathrm{\varnothing }$.

For each $i$, let ${\mathrm{\Omega }}_i$ be the explicit finite-intensity mixed-binomial space from [F2] for ${\nu }_i$ (a one-point space when ${\nu }_i=0$), with law $P_i$ and coordinate counting measure ${\eta }_i$. The countable product theorem [F3], under [A1]-[A2], supplies a probability space on which all these coordinates are independent. Each ${\eta }_i$ is supported on $A_i$ almost surely: its count on $S\setminus A_i$ is Poisson with mean zero by [F2], hence zero almost surely.

Let $E={\bigcap }_{i\ge 1}\{{\eta }_i(S\setminus A_i)=0\}$. Each event in this intersection is measurable by the coordinate evaluation maps and has probability one by step 2.1; countable subadditivity applied to their null complements gives $\mathbb{P}(E)=1$. For Borel $B$, define $\eta (B)={\sum }_{i\ge 1}{\eta }_i(B)$ on $E$ and $\eta (B)=0$ off $E$. On $E$ the countable sum is a measure by [F4], while off $E$ it is the zero measure; its evaluations are measurable as the restriction to the measurable event $E$ of increasing limits of finite sums. On $E$ it is a counting measure because the coordinate construction lists finitely many point locations per cell and the countable union of those lists is countable; off $E$ the empty configuration is a counting measure. On $E$, if $C$ is compact, [F1] gives $C\subseteq K_m$ for some $m$; then $\eta (C)={\sum }_{i=1}^m{\eta }_i(C)<\mathrm{\infty }$, because later cells avoid $K_m$ and each of the first $m$ coordinates contains finitely many points. Off $E$ all compact counts are zero. Thus $\eta$ is a measurable point process with locally finite realizations everywhere, and agrees almost surely with the unmodified superposition, preserving all its count laws.

Fix pairwise-disjoint Borel sets $B_1,\dots ,B_r$ and write $N_{ij}={\eta }_i(B_j)$ and $a_{ij}={\nu }_i(B_j)$. By [F2], within each row $i$ the $N_{ij}$ are independent Poisson variables of means $a_{ij}$; rows are independent by [F3] and [A1]-[A2], so all finitely many variables in the first $n$ rows are independent. For independent $X\sim \mathrm{Pois}(a)$ and $Y\sim \mathrm{Pois}(b)$, direct convolution gives $\mathbb{P}(X+Y=k)=e^{-(a+b)}{\sum }_{l=0}^k{a}^l{b}^{k-l}\mathrm{/}(l!(k-l)!)=e^{-(a+b)}(a+b{)}^k\mathrm{/}k!$ by the binomial theorem. Iterating this identity shows that $N_j^{(n)}={\sum }_{i=1}^n{N}_{ij}$ are independent across $j$ with laws $\mathrm{Pois}(a_j^{(n)})$, where $a_j^{(n)}={\sum }_{i=1}^n{a}_{ij}$.

On the probability-one event $E$ from step 3.1, the counts $N_j^{(n)}$ increase to $N_j=\eta (B_j)$ and $a_j^{(n)}\uparrow a_j:=\nu (B_j)$. For finite $a_j$, the events $\{N_j^{(n)}\le k_j\text{ for every }j\}$ decrease to $\{N_j\le k_j\text{ for every }j\}$; continuity from above follows by applying [F4] to their complementary increasing indicators. Their probabilities, computed from step 3.2, converge to ${\prod }_j{\sum }_{k=0}^{k_j}{e}^{-a_j}{a}_j^k\mathrm{/}k!$. Inclusion-exclusion over the finitely many lower rectangles then gives the product of Poisson point masses for every count vector, proving independence and the desired laws when all $a_j<\mathrm{\infty }$.

If $a_j=\mathrm{\infty }$, then for each integer $M\ge 0$, continuity from above gives $\mathbb{P}(N_j\le M)={\lim }_n{e}^{-a_j^{(n)}}{\sum }_{k=0}^M(a_j^{(n)}{)}^k\mathrm{/}k!=0$. The limit is zero because $e^{-t}{t}^k\to 0$ for each fixed $k$, as follows from $e^t\ge t^{k+1}\mathrm{/}(k+1)!$. Hence $N_j=\mathrm{\infty }$ almost surely. Applying the finite-coordinate argument of step 4.1 to the coordinates with finite $a_j$, while the infinite-mean coordinates are almost surely constant at $+\mathrm{\infty }$, gives the required extended independent-count convention for the whole family.

Steps 3.1, 3.2, 4.1, and 5.1 prove local finiteness and the independent Poisson count laws. The only choice principles used are [A1]-[A2] for the countable product in step 2.1.