Ripley K for a homogeneous Poisson process is Euclidean ball volume

For each compact $C\subseteq {\mathbb{R}}^d$, [F6] gives $\mathbb{E}[\eta (C{)}^2]=(\rho \mathrm{\mid }C\mathrm{\mid }{)}^2+\rho \mathrm{\mid }C\mathrm{\mid }<\mathrm{\infty }$, so $\eta$ is locally square integrable and satisfies the second-order premise of the K definition [F5].

Fix a configuration event $A$. In [F1] use $h_A(x,\mu )={\mathbf{1}}_Q(x){\mathbf{1}}_A({\theta }_x(\mu +{\delta }_x)),$ which is product measurable by [F3] and the evaluation formula for adding one atom. At each occurrence $x$ of $\eta$, deletion followed by addition restores $\eta$, so the left side is $\mathbb{E}\int {\mathbf{1}}_Q(x){\mathbf{1}}_A({\theta }_x\eta )\eta (dx)$.

The right side of that Mecke identity is $\rho {\int }_Q\mathbb{P}({\theta }_x(\eta +{\delta }_x)\in A)dx=\rho \mathrm{\mid }Q\mathrm{\mid }\mathbb{P}(\eta +{\delta }_0\in A),$ because ${\theta }_x{\delta }_x={\delta }_0$ and stationarity gives . The refined Palm identity [F2] applied to ${\mathbf{1}}_Q(x){\mathbf{1}}_A(\mu )$ says that the left side in step 1.2 is $\rho \mathrm{\mid }Q\mathrm{\mid }{P}^0(A)$. Since $\mathrm{\mid }Q\mathrm{\mid }=1$ and $\rho >0$, $P^0(A)=\mathbb{P}(\eta +{\delta }_0\in A)$ for every $A$, proving the full-Palm law identity.

Under this Palm law, $\mu$ has the distribution of $\eta +{\delta }_0$. Removing the single distinguished occurrence gives $(\eta +{\delta }_0)-{\delta }_0=\eta$ even if $\eta$ has other occurrences at $0$. Therefore ${\mathbb{E}}^0[(\mu -{\delta }_0)(B[0,r])]=\mathbb{E}[\eta (B[0,r])]=\rho \mathrm{\mid }B[0,r]\mathrm{\mid }$ by [F4]. Substituting in the K definition [F5] yields $K(r)=\mathrm{\mid }B[0,r]\mathrm{\mid }$.

The endpoint $r=0$ is included: the closed ball is $\{0\}$ and the same calculation gives $K(0)={\rho }^{-1}\mathbb{E}\eta (\{0\})=0=\mathrm{\mid }\{0\}\mathrm{\mid }$. The proof uses the one-occurrence deletion convention and asserts neither diffuse-intensity simplicity nor any other simplicity property. AC and Countable Choice [A1]–[A2] are inherited supplier assumptions.