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
- Absolute and Conditional Convergence; Rearrangement; Products
- Areas of Elementary Plane Figures
- Binary Operations, Monoids, Groups and Subgroups
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Conditional Distributions and Regular Conditional Probability
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Countability Axioms and Cardinal Functions
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Lebesgue Measure on Euclidean Space
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Measurable Functions and Simple Approximation
- Measures and Their Basic Properties
- Metric Spaces
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Outer Measure and the Caratheodory Extension Theorem
- Poisson and Cox point processes
- Polynomial Rings, the Division Algorithm and Roots
- Probability Spaces Random Variables and Expectation
- Product Measures and the Fubini Tonelli Theorems
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Series: Convergence and the Nonnegative Tests
- Sigma Algebras and Borel Sets
- Signed and Complex Measures Hahn and Jordan
- Simple Field Extensions and the Construction of the Complex Numbers
- Spatial summaries and Palm laws
- Subspaces, Products, and Quotients
- Suprema and Infima
- The Lebesgue Integral and the Convergence Theorems
- The Radon Nikodym Theorem and Lebesgue Decomposition
- The Riemann Integral in Rᵐ and Jordan Content
- The Riemann Integral: Definition and Integrability
- The Topology of Euclidean Space
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Vector Spaces, Linear Subspaces, Span and Direct Sums
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
A translated lattice exposes recentering, atomic pair measures, and one-occurrence deletion
Example
Let be uniform on and define . This is a stationary simple point process on with intensity . Its full Palm law is the deterministic unit lattice. The reduced second factorial moment measure is atomic on , so no pair-correlation density exists. Replacing by shows why Palm deletion removes one occurrence at rather than all origin occurrences.
Verification
Given: , , and the definitions and theorems of Stationarity, finite intensity, and spatial ergodicity, The full Palm distribution defined by the refined Campbell identity, Second factorial and reduced second factorial moment measures, and Pair-correlation density and Ripley K-function.
[F1] Configuration measurability is tested by Borel evaluations; ; stationarity is invariance under every ; and intensity is . (Random measures and locally finite point processes, Stationarity, finite intensity, and spatial ergodicity, Recentering a point configuration at a spatial location)
[F2] Borel Lebesgue measure is translation invariant and assigns each interval its length. (Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation, A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included)
[F3] The full Palm law is characterized by . (Existence and uniqueness of the full Palm law and the refined Campbell identity)
[F4] , with distinct occurrence indices. (Second factorial and reduced second factorial moment measures)
[F5] A pair-correlation density exists only if , and . (Pair-correlation density and Ripley K-function)
[F6] The reduced-measure Palm identity is . (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 ())
For every Borel , is measurable as a countable sum of Borel functions; every compact set meets only finitely many points of each , so this is a locally finite random counting measure. For fixed , put . The map is a translation on each of and , with the two image intervals partitioning ; by [F2] it preserves uniform probability. Reindexing gives , so the process is stationary. Since exactly one lies in for every , and .
For every compact , choose an integer with . If and , then , so uniformly in . Consequently and . Both lattice processes satisfy the local square-integrability premise in the second-order and K definitions.
For every configuration event , the unit-cube Palm construction in [F3] gives There is exactly one occurrence in , and . Therefore . In particular, using the uncentered configuration in the indicator would give on the left Campbell sum almost surely, whereas the Palm-side value is ; this is why recentering cannot be dropped.
For each selected lattice occurrence , the displacements to all other occurrences are . Hence [F4] gives for bounded Borel . In particular while , so no measurable density can satisfy [F5].
Now put , so every lattice site has two occurrence indices and . A selected occurrence has one other occurrence at the same site, so . Equivalently, is concentrated on , and , so [F6] gives . Thus ; deleting both origin occurrences would incorrectly give zero.
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 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.
A finite window makes the border correction weight visible
Example
Take , radius , and observed occurrences at . The border window is : the two boundary anchors are excluded because their full closed -neighborhoods are not observed. The two eligible anchors each have one observed partner within distance .
Verification
Given: The border-estimator procedure of Border-corrected estimator for Ripley K, , , and .
[F1] ; the anchor weight is on and outside, and the output is the eligible ordered-pair sum divided by . (Border-corrected estimator for Ripley K)
[F2] For an eligible anchor, the entire closed radius- interval is inside the observation window, so all radius- 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 ())
For , the condition is equivalent to and . Therefore and the anchor weights at are respectively .
The eligible anchor at has only as a distinct occurrence within distance ; the eligible anchor at has only . Thus the ordered-pair numerator is , , , and . The border procedure returns .
The excluded anchor has a radius- interval extending to outside , so its complete neighborhood is not observed; the anchor has , 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.