Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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.

Ordinary kriging can have larger error than simple kriging

Example

Let Ω={−1,1}3 assign probability 1/8 to each sign triple, with coordinate variables U0,U1,U2. For a common mean θ∈R, let the target be Y=θ+U0 and observations be Zi=θ+Ui for i=1,2. With θ known, simple kriging predicts Y by θ and has mean-square error 1. With θ unknown, an ordinary predictor must use weights λ1+λ2=1; its minimum mean-square error is 3/2, attained by λ1=λ2=1/2. This is a finite-model comparison, not a general inequality between ordinary and simple kriging.

Facts & Assumptions

Given: The equal-weight product space and the target and observation model in the example.

[F1]

Simple, ordinary, and universal kriging: a known-mean predictor uses the centered observations.

[F2]

Simple, ordinary, and universal kriging: ordinary-kriging weights are constrained to sum to one.

[F3]

Kriging systems and mean-square optimality: with positive-definite observation covariance, the simple minimizing weight is Σ−1c0.

[F4]

Kriging systems and mean-square optimality: under the full-rank constant-mean design, the ordinary system and error formula apply.

[F5]

Finite probability spaces, outcome weights, events, and event probabilities and Real random variables on finite probability spaces and their finite distributions: the eight sign triples have equal weight and the coordinates are real random variables on that space.

[F7]

Variance, standard deviation, and covariance on a finite probability space: variance and covariance are centered second moments.

Verification

Given: The three sign-coordinate variables on the equal-weight eight-outcome space.

1.1givenF5F6F7algebra

Each Ui has mean zero and second moment one by [F5] and [F6]. For i≠j, each sign pair occurs equally often, so [F7] gives Cov⁡(Ui,Uj)=0. Consequently, Σ=I2, c0=(0,0)⊤, and v0=1.

2.1F1F2F3step 1.1

When θ is known, [F3] and step 1.1 give simple weight Σ−1c0=0, so the simple minimizing predictor is θ. Its error is U0 and its mean-square error is E[U02]=1. For the ordinary model, the unbiasedness constraint is λ1+λ2=1 by [F2].

3.1F2F4F7step 1.1step 2.1algebra∎

The ordinary system in [F4] applies because step 1.1 gives Σ=I2 and the constant-mean design has full rank. Directly, the ordinary prediction error is U0−λ1U1−λ2U2. Expanding its square, all cross terms have expectation zero by step 1.1, so its mean-square error is 1+λ12+λ22. Substituting λ2=1−λ1 gives 32+2(λ1−12)2, whose unique minimum is 3/2 at λ1=λ2=1/2. Since 3/2>1, ordinary kriging has the larger error in this example.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

17 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.