Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: 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.

Exact and pseudo likelihoods for finite-window Poisson and Strauss models

Example

Use W=[0,2]2, unit-rate Poisson reference P0, empty exterior boundary, interaction radius R=1/2, activity β>0, and 0<γ≤1. Take the full admissible support to be Sβ,γ=C(W). Put N(η):=η(W),SR(η):=12((η⊗η)(DR)−N(η)),Hβ,γ(η):=−N(η)log⁡β−SR(η)log⁡γ, where DR={(u,v)∈W2:∥u−v∥2≤R}. The finite-window Gibbs density is Zβ,γ,R−1βN(η)γSR(η). At γ=1 this is the homogeneous Poisson model and its pseudolikelihood is proportional to its exact likelihood. At 0<γ<1 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; SR counts unordered pairs of distinct occurrences.

[F1]

A finite-window Gibbs law relative to P0 requires measurable support and 0<Z<∞. (Finite-window Gibbs density relative to a Poisson reference)

[F2]

The Strauss pair statistic SR is measurable (Finite-window pair counts are measurable); N(η)=η(W) is an evaluation map and is measurable by Finite-window spatial observations and configurations.

[F3]

For a positive Gibbs density g, the density ratio g(η+δu)/g(η) 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 P0 is e∣W∣−∫Wλ∏x∈ηλ(x), with multiplicity counted. (Finite-window spatial Poisson likelihood relative to unit rate)

[F6]

The scalar Poisson law has masses e−vvn/n! for finite v. (The scalar Poisson count law)

[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)

[F11]

Verification

Given: The window, reference law, boundary convention, and parameters in the Example; SR counts unordered pairs of distinct occurrences.

[F1] A finite-window Gibbs law relative to P0 requires measurable support and 0<Z<∞. (Finite-window Gibbs density relative to a Poisson reference)

[F2] The Strauss pair statistic SR is measurable. (Finite-window pair counts are measurable)

[F3] For a positive Gibbs density g, the density ratio g(η+δu)/g(η) 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 P0 is e∣W∣−∫Wλ∏x∈ηλ(x), with multiplicity counted. (Finite-window spatial Poisson likelihood relative to unit rate)

[F6] The scalar Poisson law has masses e−vvn/n! for finite v. (The scalar Poisson count law)

[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)

[F11] The real exponential is strictly increasing and exp⁡(0)=1. (The real exponential function and the number e by a power series, The exponential function is strictly increasing)

1.1givenF1F2F6F9F10algebraconstruct

Both N and SR are finite nonnegative integer-valued measurable functions by [F2]. For m,k∈N0, the set {N=m,SR=k} is measurable, and on it Hβ,γ=−mlog⁡β−klog⁡γ and w=βmγk. Thus both the energy and weight are measurable by their countable measurable level-set partitions. By [F10], e−Hβ,γ(η)=w(η). Since 0<γ≤1, 0<w(η)≤βN(η). The unit-rate reference count N has law Pois⁡(4) by [F9], with masses given by [F6], so Z=EP0w(η)≤EP0βN=e−4∑n=0∞(4β)nn!=e4(β−1)<∞. The empty configuration contributes P0{η=0}=e−4 to Z, hence Z≥e−4>0. Thus [F1] defines the stated Gibbs law.

2.1givenstep 1.1F2F3algebra

Inserting u adds one point and creates exactly TR(u,η):=η({v∈W:∥v−u∥2≤R}) unordered interaction pairs, counting occurrences: if the pair count is written as the number of unordered pairs, the increase is SR(η+δu)−SR(η)=(2TR(u,η)+1−1)/2=TR(u,η); the 1 in the numerator is the new diagonal term removed in the definition of SR. Therefore w(η+δu)w(η)=βγTR(u,η). The same ratio holds for the normalized density because Z cancels; [F3] shows that the Strauss Papangelou conditional intensity is λ(u;η)=βγTR(u,η).

2.2givenstep 1.1F1F7F8construct

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.

3.1step 1.1step 2.1F4F5algebra

When γ=1, SR drops out and the normalizer from the earlier calculation gives Z=e4(β−1), so the exact density is e4(1−β)βN(η), matching the Poisson formula [F5]. The Papangelou intensity is the constant β, so [F4] gives pseudolikelihood βN(η)e−4β. The ratio of exact to pseudo likelihood is the observation-independent constant e4.

3.2givenstep 2.1F1F4algebra

Now suppose 0<γ<1, let x=(1,1), and compare the empty configuration 0 with δx. By [F1] and the fact that neither configuration has an interacting pair, their exact Gibbs density ratio is g(δx)/g(0)=β. By [F4] and step 2.1, the pseudolikelihood ratio is PL⁡(δx)PL⁡(0)=βexp⁡{β(1−γ)a},a:=∣{u∈W:∥u−x∥2≤R}∣. Indeed the event factor at x is β, and the integrated intensity changes from β∣W∣ to β(∣W∣−(1−γ)a).

4.1step 3.2F11F12algebra∎

The square [4/5,6/5]2 lies inside the radius-1/2 ball about x, so a≥4/25>0 by [F12]. Hence exp⁡{β(1−γ)a}>1 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

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