Alphabeta Math
Pipeline-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.

Spatial summaries and Palm laws — Examples

1 · Prerequisites

2 · Summary

A uniformly translated one-dimensional lattice is stationary but has an atomic reduced second factorial measure, so a pair-correlation density need not exist. Doubling each lattice site makes one-occurrence Palm deletion visible at radius zero. A finite-window calculation shows which anchors the border procedure retains and how its ordered-pair sum is normalized; it does not establish estimator unbiasedness.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-adaptedOpen item page →

A translated lattice exposes recentering, atomic pair measures, and one-occurrence deletion

Example

Let U be uniform on [0,1) and define ηU=∑k∈Zδk+U. This is a stationary simple point process on R with intensity 1. Its full Palm law is the deterministic unit lattice. The reduced second factorial moment measure is atomic on Z∖{0}, so no pair-correlation density exists. Replacing ηU by 2ηU shows why Palm deletion removes one occurrence at 0 rather than all origin occurrences.

Verification

[F1] Configuration measurability is tested by Borel evaluations; θxμ(B)=μ(B+x); stationarity is invariance under every θx; and intensity is Eη(Q). (Random measures and locally finite point processes, Stationarity, finite intensity, and spatial ergodicity, Recentering a point configuration at a spatial location)

[F3] The full Palm law is characterized by E∫h(x,θxη)η(dx)=ρ∫∫h(x,μ)P0(dμ)dx. (Existence and uniqueness of the full Palm law and the refined Campbell identity)

[F4] αred(2)(D)=E∑i≠j1Q(Xi)1D(Xj−Xi), with distinct occurrence indices. (Second factorial and reduced second factorial moment measures)

[F5] A pair-correlation density exists only if αred(2)(du)=ρ2g(u)du, and K(0)=ρ−1E0[(μ−δ0)({0})]. (Pair-correlation density and Ripley K-function)

[F6] The reduced-measure Palm identity is αred(2)(D)=ρE0[(μ−δ0)(D)]. (The reduced second factorial moment measure is the Palm expectation after one-occurrence deletion)

[A1] AC and Countable Choice are inherited through the point-process and Palm supplier dependency closure; the explicit lattice calculations use no choices. (The Axiom of Choice, The Axiom of Countable Choice (ACω))

1.1givenF1F2constructalgebra

For every Borel B, u↦ηu(B)=∑k∈Z1B(k+u) is measurable as a countable sum of Borel functions; every compact set meets only finitely many points of each ηu, so this is a locally finite random counting measure. For fixed x, put t=x−⌊x⌋∈[0,1). The map u↦{u−x} is a translation on each of [0,t) and [t,1), with the two image intervals partitioning [0,1); by [F2] it preserves uniform probability. Reindexing k∈Z gives θxηu=η{u−x}, so the process is stationary. Since exactly one k+u lies in Q=[0,1) for every u∈[0,1), ηU(Q)=1 and ρ=1.

2.1step 1.1givenF4F5algebra

For every compact C⊆R, choose an integer m≥1 with C⊆[−m,m]. If u∈[0,1) and k+u∈C, then −m−1≤k≤m, so ηu(C)≤2m+2 uniformly in u. Consequently E[ηU(C)2]≤(2m+2)2<∞ and E[(2ηU)(C)2]≤4(2m+2)2<∞. Both lattice processes satisfy the local square-integrability premise in the second-order and K definitions.

2.2F1F3step 1.1

For every configuration event A, the unit-cube Palm construction in [F3] gives P0(A)=E∫Q1A(θxηU)ηU(dx). There is exactly one occurrence x=U in Q, and θUηU=∑k∈Zδk=:Λ. Therefore P0=δΛ. In particular, using the uncentered configuration in the indicator 1{μ({0})>0} would give 0 on the left Campbell sum almost surely, whereas the Palm-side value is 1; this is why recentering cannot be dropped.

3.1F4F5step 1.1step 2.1

For each selected lattice occurrence Xi=k+U∈Q, the displacements to all other occurrences are Z∖{0}. Hence [F4] gives αred(2)(D)=#(D∩(Z∖{0})) for bounded Borel D. In particular αred(2)({1})=1 while ∣{1}∣=0, so no measurable density g can satisfy [F5].

3.2F4F5F6step 2.1step 2.2algebra

Now put η~U=2ηU, so every lattice site has two occurrence indices and ρ~=2. A selected occurrence has one other occurrence at the same site, so αred(2)({0})=2. Equivalently, P0 is concentrated on 2Λ, and μ({0})=2, so [F6] gives 2=ρ~E0[(μ−δ0)({0})]=2⋅1. Thus K(0)=1/2; deleting both origin occurrences would incorrectly give zero.

4.1A1step 2.1step 2.2step 3.1step 3.2∎

The simple lattice has an atomic reduced measure and no pair-correlation density, while the doubled lattice verifies that factorial pairs distinguish occurrence indices and Palm deletion removes exactly one occurrence. The origin-centered convention and the closed-ball endpoint r=0 are both used explicitly. AC and Countable Choice [A1] are inherited assumptions only.

Sources

Last and Penrose, Exercises 8.3, 8.10–8.11 and Theorem 9.1; Baddeley, Example 2.15 and Lecture 3, §3.3. Every lattice and multiplicity calculation is verified above.

ExampleConstruction: AI-generatedVerification: AI-adaptedOpen item page →

A finite window makes the border correction weight visible

Example

Take W=[0,1]⊂R, radius r=1/4, and observed occurrences at 0.1,0.4,0.5,0.9. The border window is W−r=[1/4,3/4]: the two boundary anchors are excluded because their full closed r-neighborhoods are not observed. The two eligible anchors each have one observed partner within distance r.

Verification

Given: The border-estimator procedure of Border-corrected estimator for Ripley K, W=[0,1], r=1/4, and ξ=δ0.1+δ0.4+δ0.5+δ0.9.

[F1] W−r={x∈W:[x−r,x+r]⊆W}; the anchor weight is 1 on W−r and 0 outside, and the output is the eligible ordered-pair sum divided by ρ^N(W−r). (Border-corrected estimator for Ripley K)

[F2] For an eligible anchor, the entire closed radius-r interval is inside the observation window, so all radius-r partner occurrences are observed. (Border-corrected estimator for Ripley K)

[A1] AC and Countable Choice are inherited through the estimator's K and point-process dependencies; this finite calculation uses no choices. (The Axiom of Choice, The Axiom of Countable Choice (ACω))

1.1F1constructalgebra

For x∈[0,1], the condition [x−1/4,x+1/4]⊆[0,1] is equivalent to x≥1/4 and x≤3/4. Therefore W−r=[1/4,3/4] and the anchor weights at 0.1,0.4,0.5,0.9 are respectively 0,1,1,0.

2.1step 1.1F1algebra

The eligible anchor at 0.4 has only 0.5 as a distinct occurrence within distance 1/4; the eligible anchor at 0.5 has only 0.4. Thus the ordered-pair numerator is 2, N(W−r)=2, N(W)=4, and ρ^=4/∣W∣=4. The border procedure returns 2/(4⋅2)=1/4.

3.1A1step 1.1step 2.1F2∎

The excluded anchor 0.1 has a radius-1/4 interval extending to −0.15 outside W, so its complete neighborhood is not observed; the anchor 0.4 has [0.15,0.65]⊆W, as guaranteed by [F2]. This calculation verifies the procedure's edge-exposure rule only and proves no finite-sample unbiasedness claim. AC and Countable Choice [A1] are inherited supplier assumptions.

Sources

Baddeley, Lecture 2, §2.6, formula (18); Last and Penrose, Chapter 8, spatial K-function discussion. This is a geometric example, not an unbiasedness result.

Sources