TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Finite-window spatial Poisson likelihood relative to unit rate

Statement

Let $W \subset R^{d}$ and $C (W)$ be as in Finite-window spatial observations and configurations, with volume $v = ∣ W ∣ < \infty$ . For each parameter $θ$ , let $λ_{θ} : W \to [0, \infty)$ be a finite-valued Borel function and assume $Λ_{θ} : = \int_{W} λ_{θ} (x) ℓ_{W} (d x) < \infty .$ Extend $λ_{θ}$ by zero off $W$ and let $P_{θ}$ be the law on $C (W)$ of the Poisson process on $R^{d}$ with intensity measure $ν_{θ} = 1_{W} λ_{θ} d ℓ_{d}$ . Let $P_{0}$ be the unit-rate Poisson law on $C (W)$ obtained from intensity $1_{W} d ℓ_{d}$ . Then $\frac{d P_{θ}}{d P_{0}} (η) = g_{θ} (η) : = \exp {v - Λ_{θ}} \prod_{x \in η} λ_{θ} (x) .$ where the product counts atom occurrences and the empty product is $1$ . In particular $P_{θ} ≪ P_{0}$ . This formula explicitly chooses a common parameter-indexed density version, so it requires no arbitrary simultaneous selection of Radon–Nikodym representatives.

For an observed $η$ , if every observed occurrence has positive intensity, the log likelihood, up to the parameter-independent term $v$ , is $ℓ_{η} (θ) = \sum_{x \in η} \log λ_{θ} (x) - Λ_{θ} .$ If any observed occurrence has zero intensity, the likelihood is zero and its log is $- \infty$ .

Facts & Assumptions

Given: The window $W$ , the parameter-indexed intensities, and their finite integrals as in the Statement.

[F1]

$C (W)$ is the finite-window configuration space, with boundary points included exactly when they belong to $W$ ; $v = ℓ_{W} (W) < \infty$ . (Finite-window spatial observations and configurations)

[F2]

A nonnegative measurable density $f$ relative to a measure $μ$ defines the measure $f d μ$ , and its total mass is $\int f d μ$ . (The measure with density $f$ relative to $μ$ )

[F3]

The law of a Poisson process with finite intensity $ν$ is the push-forward of $\sum_{n \geq 0} e^{- ν (W)} ν (W)^{n} / n! (ν / ν (W))^{\otimes n}$ under $(x_{1}, \dots, x_{n}) \mapsto \sum_{i} δ_{x_{i}}$ ; the zero-intensity case is the empty process. (Finite-intensity Poisson-process existence and mixed-binomial law)

[F4]

For a finite measure with density $f$ , the $n$ -fold product has density $\prod_{i = 1}^{n} f (x_{i})$ relative to the $n$ -fold product of the reference measure. (Finite products of measures with densities have the product density)

[F5]

The occurrence product $η \mapsto \prod_{x \in η} f (x)$ is measurable for every finite-valued Borel $f$ . (Products of a measurable intensity over finite configurations are measurable)

[F6]

In a dominated experiment the supplied reference measure is fixed, and a likelihood density at the observation is a chosen density version evaluated there. (Dominated statistical experiments, Likelihood densities)

[F7]

For positive arguments, $\log (x y) = \log x + \log y$ and $\log (\exp t) = t$ . (The natural logarithm as the inverse of the exponential function, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm)

Proof

Given: $λ_{θ}$ is finite-valued Borel and $\int_{W} λ_{θ} d ℓ_{W} = Λ_{θ} < \infty$ .

1.1givenF1F2F3

The zero extension of $λ_{θ}$ is Borel: for Borel $E \subseteq [0, \infty)$ its inverse image is $W \cap λ_{θ}^{- 1} (E)$ if $0 \notin E$ , and $W^{c} \cup (W \cap λ_{θ}^{- 1} (E))$ if $0 \in E$ ; both are Borel because $W$ is Borel and $λ_{θ}$ is Borel on $W$ . Thus [F2] defines its finite measure of total mass $Λ_{θ}$ on $R^{d}$ , supported on $W$ . The unit-rate reference intensity $1_{W} d ℓ_{d}$ has total mass $v$ by [F1]. Thus [F3] applies to both Poisson laws, and their finite-mixture tuple integrals are supported on $W^{n}$ .

1.2givenF5construct

The product factor in $g_{θ}$ is measurable by [F5], and the exponential factor is a finite nonnegative constant. Hence $g_{θ}$ is a measurable nonnegative function on $C (W)$ .

2.1step 1.1F3F4

Let $A \subseteq C (W)$ be measurable. Expanding [F3] for $P_{θ}$ on its support $W$ and using [F4] gives $P_{θ} (A) = e^{- Λ_{θ}} \sum_{n = 0}^{\infty} \frac{1}{n!} \int_{W^{n}} 1_{A} ⁣ (\sum_{i = 1}^{n} δ_{x_{i}}) \prod_{i = 1}^{n} λ_{θ} (x_{i}) ℓ_{W}^{\otimes n} (d (x_{1}, \dots, x_{n})) .$ For $P_{0}$ , the same formula holds with $Λ_{θ}$ replaced by $v$ and every product factor replaced by $1$ .

3.1step 2.1F3F4algebra

Expand $\int_{A} g_{θ} d P_{0}$ by the $P_{0}$ formula in step 2.1. On the $n$ -tuple component, $g_{θ} (\sum_{i} δ_{x_{i}}) = e^{v - Λ_{θ}} \prod_{i} λ_{θ} (x_{i})$ , including $n = 0$ by the empty-product convention. Cancellation of $e^{- v}$ with $e^{v}$ yields exactly the series for $P_{θ} (A)$ in step 2.1.

4.1step 1.2step 3.1F6F7algebra∎

Since step 3.1 holds for every measurable $A$ , $g_{θ}$ is a Radon–Nikodym density of $P_{θ}$ relative to $P_{0}$ , and therefore $P_{θ} ≪ P_{0}$ . The explicitly displayed $g_{θ}$ supplies the density version for every $θ$ , so the arbitrary selector in [F6] is not used. Taking its logarithm gives the stated expression when all event factors are positive; a zero factor makes the finite product zero and the log likelihood $- \infty$ .

Depends on

Used by

Dependency tree · two levels

55 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Adrian Baddeley, Spatial Point Processes and their Applications, complete lecture notes (standard reference, not scraped)
Günter Last and Mathew Penrose, Lectures on the Poisson Process, author-hosted 2017 version (standard reference, not scraped)