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.
Exact and pseudo likelihoods for finite-window Poisson and Strauss models
Example
Use , unit-rate Poisson reference , empty exterior boundary, interaction radius , activity , and . Take the full admissible support to be . Put where . The finite-window Gibbs density is . At this is the homogeneous Poisson model and its pseudolikelihood is proportional to its exact likelihood. At the two criteria are not proportional as functions of the observation.
Facts & Assumptions
Given: The window, reference law, boundary convention, and parameters in the Example; counts unordered pairs of distinct occurrences.
A finite-window Gibbs law relative to requires measurable support and . (Finite-window Gibbs density relative to a Poisson reference)
The Strauss pair statistic is measurable (Finite-window pair counts are measurable); is an evaluation map and is measurable by Finite-window spatial observations and configurations.
For a positive Gibbs density , the density ratio is its Papangelou conditional intensity. (A positive finite-window Gibbs density has its density-ratio Papangelou intensity)
The pseudolikelihood is the product of deleted-point Papangelou factors times the exponential integrated-intensity term. (Finite-window point-process pseudolikelihood)
The finite Poisson likelihood relative to is , with multiplicity counted. (Finite-window spatial Poisson likelihood relative to unit rate)
The scalar Poisson law has masses for finite . (The scalar Poisson count law)
Every singleton in has Lebesgue measure zero by the degenerate-box case. (A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included)
A finite Poisson process with atomless intensity is simple almost surely. (A finite Poisson process with atomless intensity is simple)
A Poisson process count on a set of finite intensity has the scalar Poisson law with that intensity as its parameter. (Poisson and Cox point processes)
The real exponential is strictly increasing and . (The real exponential function and the number by a power series, The exponential function is strictly increasing)
Lebesgue measure is monotone, and the box has volume . (Measures are monotone, A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included)
Verification
Given: The window, reference law, boundary convention, and parameters in the Example; counts unordered pairs of distinct occurrences.
[F1] A finite-window Gibbs law relative to requires measurable support and . (Finite-window Gibbs density relative to a Poisson reference)
[F2] The Strauss pair statistic is measurable. (Finite-window pair counts are measurable)
[F3] For a positive Gibbs density , the density ratio is its Papangelou conditional intensity. (A positive finite-window Gibbs density has its density-ratio Papangelou intensity)
[F4] The pseudolikelihood is the product of deleted-point Papangelou factors times the exponential integrated-intensity term. (Finite-window point-process pseudolikelihood)
[F5] The finite Poisson likelihood relative to is , with multiplicity counted. (Finite-window spatial Poisson likelihood relative to unit rate)
[F6] The scalar Poisson law has masses for finite . (The scalar Poisson count law)
[F7] Every singleton in has Lebesgue measure zero by the degenerate-box case. (A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included)
[F8] A finite Poisson process with atomless intensity is simple almost surely. (A finite Poisson process with atomless intensity is simple)
[F9] A Poisson process count on a set of finite intensity has the scalar Poisson law with that intensity as its parameter. (Poisson and Cox point processes)
[F10] for and exponentials satisfy . (The natural logarithm as the inverse of the exponential function, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm, The exponential addition formula )
[F11] The real exponential is strictly increasing and . (The real exponential function and the number by a power series, The exponential function is strictly increasing)
[F12] Lebesgue measure is monotone, and the box has volume . (Measures are monotone, A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included)
Both and are finite nonnegative integer-valued measurable functions by [F2]. For , the set is measurable, and on it and . Thus both the energy and weight are measurable by their countable measurable level-set partitions. By [F10], . Since , . The unit-rate reference count has law by [F9], with masses given by [F6], so The empty configuration contributes to , hence . Thus [F1] defines the stated Gibbs law.
Inserting adds one point and creates exactly unordered interaction pairs, counting occurrences: if the pair count is written as the number of unordered pairs, the increase is ; the in the numerator is the new diagonal term removed in the definition of . Therefore The same ratio holds for the normalized density because cancels; [F3] shows that the Strauss Papangelou conditional intensity is .
Every singleton is a degenerate box of Lebesgue measure zero by [F7], so the unit-rate reference intensity is atomless. It is simple almost surely by [F8]. The normalized Strauss law is absolutely continuous with respect to that reference and is therefore also supported on simple configurations. Thus on a probability-one set the occurrence-pair energy is the usual simple-pattern Strauss energy.
When , drops out and the normalizer from the earlier calculation gives , so the exact density is , matching the Poisson formula [F5]. The Papangelou intensity is the constant , so [F4] gives pseudolikelihood . The ratio of exact to pseudo likelihood is the observation-independent constant .
Now suppose , let , and compare the empty configuration with . By [F1] and the fact that neither configuration has an interacting pair, their exact Gibbs density ratio is . By [F4] and step 2.1, the pseudolikelihood ratio is Indeed the event factor at is , and the integrated intensity changes from to .
The square lies inside the radius- ball about , so by [F12]. Hence by [F11], and the pseudo ratio is strictly larger than the exact ratio . A constant multiple of the exact likelihood would have equal observation ratios, so the Strauss pseudolikelihood is not the joint likelihood in this case. The example makes no consistency or asymptotic claim.
Depends on
- Finite-window spatial observations and configurations
- Finite-window pair counts are measurable
- Finite-window Gibbs density relative to a Poisson reference
- Papangelou conditional intensity on a finite window
- Finite-window point-process pseudolikelihood
- A finite Poisson process with atomless intensity is simple
- Finite-window spatial Poisson likelihood relative to unit rate
- A positive finite-window Gibbs density has its density-ratio Papangelou intensity
- Poisson and Cox point processes
- The scalar Poisson count law
- The real exponential function and the number $e$ by a power series
- The natural logarithm as the inverse of the exponential function
- Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm
- The exponential addition formula $\exp(x+y)=\exp(x)\exp(y)$
- The exponential function is strictly increasing
- A box in $\mathbb{R}^n$ with parameters $a_i\le b_i$ is Lebesgue measurable of measure $\prod_{i<n}(b_i-a_i)$, whichever of its faces are included
- Measures are monotone
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
90 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)