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.

Asymptotic unbiasedness of lattice covariance and variogram estimators

Statement

Let $(Y_{j})_{j \in Z^{d}}$ be real square-integrable random variables with constant mean $E [Y_{j}] = μ$ and lag-dependent covariance $C (h) = Cov (Y_{j + h}, Y_{j})$ independent of $j$ . Let $(V_{n})$ be nonempty finite observation windows and assume that their sample means from Lagged lattice covariance and variogram estimators satisfy ${\overset{ˉ}{Y}}_{n} \to μ$ in $L^{2}$ . For each fixed $h \in Z^{d}$ with $N_{n} (h) > 0$ eventually, the pair-count-normalized raw-product covariance estimator satisfies $E [{\hat{C}}_{n} (h)] ⟶ C (h) .$

Separately, if the second moment of the lag- $h$ increment is independent of $j$ and equals $2 γ (h) < \infty$ , then the empirical semivariogram from Lagged lattice covariance and variogram estimators is exactly unbiased: $E [{\hat{γ}}_{n} (h)] = γ (h)$ for every $n$ with $N_{n} (h) > 0$ . These are expectation statements only; they assert no variance consistency, weak consistency, or central limit theorem.

Facts & Assumptions

Given: The lattice field, windows, fixed lag, and $L^{2}$ -consistent sample means in the Statement.

[A1]

Lagged lattice covariance and variogram estimators: for $P_{n} (h) = {j \in V_{n} : j + h \in V_{n}}$ and $N_{n} (h) = ∣ P_{n} (h) ∣$ , ${\hat{C}}_{n} (h) = \frac{1}{N_{n} (h)} \sum_{j \in P_{n} (h)} Y_{j} Y_{j + h} - {\overset{ˉ}{Y}}_{n}^{2},$ and ${\hat{γ}}_{n} (h) = \frac{1}{2 N_{n} (h)} \sum_{j \in P_{n} (h)} (Y_{j + h} - Y_{j})^{2} .$

[F1]

Moments, variance, and covariance on a probability space: for square-integrable real random variables, covariance is the expectation of the centered product.

[F2]

Linearity, monotonicity, and the modulus bound for expectation: expectation is linear on finite sums of integrable variables, and $∣ E [Z] ∣ \leq E [∣ Z ∣]$ for integrable $Z$ .

[F3]

Cauchy-Schwarz for random variables: for square-integrable $U, V$ , $E [∣ U V ∣] \leq ∥ U ∥_{2} ∥ V ∥_{2} < \infty$ , so $U V$ is integrable.

[F4]

$L^{p}$ convergence for random variables: ${\overset{ˉ}{Y}}_{n} \to μ$ in $L^{2}$ means $∥ {\overset{ˉ}{Y}}_{n} - μ ∥_{2} \to 0$ .

Proof

technique · direct finite-sum expectation calculation

1.1givenF1F3algebra

Every product $Y_{j} Y_{j + h}$ is integrable by [F3]. By the stationary covariance identity in the Given and [F1], $E [Y_{j} Y_{j + h}] = C (h) + μ^{2}$ for every $j$ .

1.2F2F3F4algebra

By [F2], [F3] and [F4], $∣ E [{\overset{ˉ}{Y}}_{n}^{2}] - μ^{2} ∣ = ∣ E [({\overset{ˉ}{Y}}_{n} - μ) ({\overset{ˉ}{Y}}_{n} + μ)] ∣ \leq ∥ {\overset{ˉ}{Y}}_{n} - μ ∥_{2} ∥ {\overset{ˉ}{Y}}_{n} + μ ∥_{2} ⟶ 0,$ because $∥ {\overset{ˉ}{Y}}_{n} + μ ∥_{2}^{2} \leq 2 ∥ {\overset{ˉ}{Y}}_{n} - μ ∥_{2}^{2} + 8 μ^{2}$ is bounded by $(a + b)^{2} \leq 2 a^{2} + 2 b^{2}$ and [F4].

2.1A1F2step 1.1step 1.2

Applying [F2] to the finite average in [A1] and using step 1.1 gives $E [{\hat{C}}_{n} (h)] = C (h) + μ^{2} - E [{\overset{ˉ}{Y}}_{n}^{2}] .$ Step 1.2 therefore proves $E [{\hat{C}}_{n} (h)] \to C (h)$ .

3.1A1F2givenalgebra∎

Under the increment-moment hypothesis, every summand in [A1] has expectation $2 γ (h)$ . Linearity [F2] over the $N_{n} (h)$ pairs and division by $2 N_{n} (h)$ give $E [{\hat{γ}}_{n} (h)] = γ (h)$ whenever the pair count is positive.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 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

Evgeny Spodarev, Spatial Statistics: Lecture Notes (2024), Lemma 2.8 and Section 2.2 (standard reference, not scraped)
Dennis Sun, Stanford Stats 253 Lecture 6: Covariance Estimation (2014), pp. 8–15 (standard reference, not scraped)