Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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.

Classical error attenuates the simple linear regression slope

Statement

Let X,U,ϵ,W,Y be square-integrable real random variables on one probability space with E[X]=E[U]=E[ϵ]=0, U independent of the random element (X,ϵ), and ϵ independent of X. Set W=X+U,Y=α+βX+ϵ,α,β∈R, so W has classical additive error. If Var⁡(X)+Var⁡(U)>0, the coefficient γ of the best affine L2 predictor of Y from W is γ=Cov⁡(Y,W)Var⁡(W)=βVar⁡(X)Var⁡(X)+Var⁡(U). The attenuation factor lies in [0,1]. When both variances are positive, it is strictly between 0 and 1, so for β≠0 the coefficient has the same sign as β and smaller absolute value; when β=0, γ=0. The boundary cases are: if Var⁡(X)=0, the factor is 0; if Var⁡(U)=0 and Var⁡(X)>0, it is 1.

Facts & Assumptions

Given: The square-integrable centered variables and independence hypotheses in the Statement.

[F1]

The classical model has W=X+U, with centered U independent of X (Additive measurement error and categorical misclassification models).

[F2]

Variance and covariance are the centered-square and centered-product expectations (Moments, variance, and covariance on a probability space).

[F3]

Covariance is bilinear on finite linear combinations, including constants (Covariance is symmetric and bilinear in finite linear combinations).

[F4]

Independence of random variables means independence of their generated sigma-algebras (Independent random elements).

[F5]

For a finite independent family of integrable real random variables, the expectation of their product factors and the product is integrable (Expectation factors over a finite product of mutually independent random variables).

[F6]

The best affine L2 predictor satisfies the covariance normal equations; with one predictor W, its slope satisfies γVar⁡(W)=Cov⁡(Y,W) (Normal equations for best affine L2 prediction).

[F7]

Square-integrable real variables are integrable on a probability space: apply Cauchy-Schwarz with the constant-one variable (Cauchy-Schwarz for random variables).

Proof

1.1givenF2F4F5F7

By [F7] the variables are integrable. Independence of U from (X,ϵ) implies independence of U from each coordinate, because the coordinate sigma-algebras are contained in that of the pair; together with ϵ independent of X, [F4] and [F5] give E[XU]=E[ϵU]=E[Xϵ]=0. Centering and [F2] therefore give Cov⁡(X,U)=Cov⁡(ϵ,U)=Cov⁡(X,ϵ)=0.

2.1givenF1F2F3step 1.1algebra

By [F1], W=X+U; by bilinearity [F3] and the zero covariances in step 1.1, Cov⁡(Y,W)=Cov⁡(α+βX+ϵ,X+U)=βVar⁡(X). The same expansion gives Var⁡(W)=Var⁡(X)+2Cov⁡(X,U)+Var⁡(U)=Var⁡(X)+Var⁡(U).

3.1givenF6step 2.1algebra

The variance sum is positive by hypothesis, so [F6] determines the unique slope γ=Cov⁡(Y,W)/Var⁡(W). Substitution from step 2.1 gives the displayed formula.

4.1givenstep 3.1algebra∎

Nonnegative variances and a positive sum give 0≤Var⁡(X)/(Var⁡(X)+Var⁡(U))≤1. Equality at 0 occurs exactly when Var⁡(X)=0; equality at 1 occurs exactly when Var⁡(U)=0. When both are positive the factor is strictly between the endpoints, so for β≠0 step 3.1 gives a coefficient of the same sign and smaller absolute value; when β=0, step 3.1 gives γ=0, so no strict reduction holds. This proves the stated attenuation and boundary cases.

Depends on

Used by

Dependency tree · two levels

23 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