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

Bias–variance decomposition

Statement

In a statistical experiment, let ψ:Θ→R and let T be a real estimator with Eθ[T2]<∞. For every θ, MSE⁡θ(T)=Var⁡θ(T)+Bias⁡θ(T)2.

Facts & Assumptions

Given: A statistical experiment, a real estimand ψ, and an estimator T that is square-integrable under each parameter law considered.

[F1]

Bias is Eθ[T]−ψ(θ) and MSE is Eθ[(T−ψ(θ))2]. (Bias and mean squared error)

[F2]

For square-integrable real T, Var⁡θ(T)=Eθ[(T−EθT)2]. (Moments, variance, and covariance on a probability space)

[F3]

The Lebesgue integral is linear on finite linear combinations of integrable functions. (The Lebesgue integral is linear on L1(μ))

[F4]

Cauchy–Schwarz gives ∫∣fg∣ dμ≤∥f∥2∥g∥2 for square-integrable f,g. (Cauchy-Schwarz inequality for L2)

Proof

technique · direct
1.1givenF1F4

Fix θ. Since Pθ is a probability measure, the constant 1 has L2(Pθ) norm 1. Applying [F4] to T and 1 gives Eθ∣T∣≤(Eθ[T2])1/2<∞. Put μ=Eθ[T] and b=μ−ψ(θ). Then [F1] gives b=Bias⁡θ(T) and T−ψ(θ)=(T−μ)+b.

2.1step 1.1F1F2F3algebra∎

Since T,μ∈L1(Pθ) by step 1.1 and Pθ(X)=1, [F3] gives Eθ[T−μ]=Eθ[T]−μEθ[1]=0. For every finite c, (T−c)2≤2T2+2c2, so the centered square and squared error are integrable. Expanding (T−ψ(θ))2=((T−μ)+b)2 now gives MSE⁡θ(T)=Eθ[(T−μ)2]+b2=Var⁡θ(T)+Bias⁡θ(T)2 by [F1] and [F2].

Depends on

Used by

Dependency tree · two levels

15 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