TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Gaussian simple kriging is a conditional mean

Statement

Assume the Axiom of Choice. Let $X$ be a Gaussian real field, meaning every finite coordinate vector has a possibly singular multivariate-normal law. For the target $Y = X (s_{0})$ and observations $Z$ of Simple, ordinary, and universal kriging, suppose $Σ$ is positive definite. Then the simple-kriging predictor $m_{0} + (Σ^{- 1} c_{0})^{⊤} (Z - m)$ equals $E [Y ∣ σ (Z)]$ almost surely, where $σ (Z)$ is the sigma-algebra generated by the observation vector.

Facts & Assumptions

Given: AC, a finite jointly Gaussian vector $(Y, Z)$ with finite second moments, and positive-definite observation covariance $Σ$ .

[A1]

The Axiom of Choice says every family of nonempty sets has a choice function. The Axiom of Choice

[F1]

Gaussian process: under AC, every finite coordinate vector of a Gaussian field has a possibly singular multivariate-normal law.

[F2]

Uncorrelated jointly Gaussian blocks are independent: under AC, jointly Gaussian finite blocks with zero cross-covariance are independent, including when a covariance matrix is singular.

[F3]

Independent random elements and Independent sigma-algebras and independent events: independent random elements generate independent sigma-algebras, so their measurable events factor.

[F4]

Kriging systems and mean-square optimality: under $Σ ≻ 0$ , the simple-kriging weights are $Σ^{- 1} c_{0}$ .

[F5]

Conditioning a known variable and an independent variable: under AC, an integrable variable whose Borel events are independent of the conditioning sigma-algebra has conditional expectation equal to its mean.

[F6]

Conditional expectation as an ae class and Conditional expectation given a sigma algebra: the conditional-expectation class consists of measurable integrable versions with the same integrals as the input on every event in the conditioning sigma-algebra.

[F7]

Conditional expectation is unique almost surely: two versions with the same conditioning sigma-algebra and event integrals agree almost surely.

Proof

Given: AC, the Gaussian field, and the target and observation vector as in the statement.

1.1A1F1F4givenalgebra

Let $λ = Σ^{- 1} c_{0}$ and $R = Y - m_{0} - λ^{⊤} (Z - m)$ . By [F1], $(R, Z)$ is jointly Gaussian because each of its linear combinations is a linear combination of $(Y, Z)$ . Its residual mean is zero, and $Cov (R, Z) = c_{0}^{⊤} - λ^{⊤} Σ = 0$ by the equation $Σ λ = c_{0}$ .

2.1A1F2step 1.1

Applying [F2] to the jointly Gaussian blocks $R$ and $Z$ from step 1.1 shows that $R$ is independent of $Z$ .

3.1A1F3F5F6step 2.1

By [F3], independence from step 2.1 gives the Borel-event factorization required by [F5] for $R$ and $G = σ (Z)$ . The residual is integrable because it is a finite linear combination of square-integrable variables. AC is stated in [A1], so [F5] gives $E [R ∣ G] = E [R] = 0$ ; by [F6], this means $E [R 1_{B}] = 0$ for every $B \in G$ .

4.1F6F7step 3.1∎

Put $\hat{Y} = m_{0} + λ^{⊤} (Z - m)$ . This is $σ (Z)$ -measurable and integrable. For each $B \in σ (Z)$ , step 3.1 and $Y = \hat{Y} + R$ give $E [Y 1_{B}] = E [\hat{Y} 1_{B}]$ . Thus [F6] makes $\hat{Y}$ a version of $E [Y ∣ σ (Z)]$ , and [F7] gives the asserted almost-sure equality. AC is used only through the Gaussian-law, Gaussian-independence, and conditional-expectation suppliers.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

38 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), Sections 3.1–3.2 (standard reference, not scraped)
Dennis Sun, Stats 253 Lecture 5: Prediction and Kriging (Stanford University) (standard reference, not scraped)