Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04
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.

Best affine prediction from one random variable

Statement

Let X and Y be square-integrable real random variables.

  • If Var⁡(Y)>0, the unique best affine predictor of X from Y is E[X]+Cov⁡(X,Y)Var⁡(Y)(Y−E[Y]).
  • If Var⁡(Y)=0, then every best affine predictor is almost surely equal to the constant E[X].

Facts & Assumptions

Given: Square-integrable real random variables X,Y.

[L1]

Best affine L2 predictors are characterized by the normal equations (Normal equations for best affine L2 prediction).

[L2]

Variance is Cov⁡(Y,Y) (Moments, variance, and covariance on a probability space).

Proof

technique · direct
1.1

With one predictor variable, the normal equation from [L1] is Cov⁡(Y,Y)a1=Cov⁡(X,Y). By [L2], this is Var⁡(Y)a1=Cov⁡(X,Y).

L1L2
2.1

If Var⁡(Y)=0, then step 1.1 makes the normal equation 0⋅a1=Cov⁡(X,Y). Hence every real a1 solves it, and [L1] says that all corresponding affine predictors yield the same optimal class. Taking a1=0 gives the constant predictor E[X], so every best affine predictor is almost surely equal to that constant.

step 1.1L1L2algebra
2.2

If Var⁡(Y)>0, step 1.1 gives a1=Cov⁡(X,Y)Var⁡(Y). Substituting this into the intercept formula from [L1] yields the displayed predictor a0+a1Y=E[X]+Cov⁡(X,Y)Var⁡(Y)(Y−E[Y]).

step 1.1L1L2algebra
3.1

Steps 2.2 and 2.1 give the positive-variance and zero-variance cases.

step 2.2step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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