Estimation.GaussMarkov

The Gauss-Markov theorem for linear models: best linear unbiased estimation under spherical errors.

QuadForm 3 core · 2 supporting This file provides the deterministic quadratic-form layer of the finite Gauss-Markov theory. ★ quadVar_spherical

Quadratic Variance Form

This file provides the deterministic quadratic-form layer of the finite Gauss-Markov theory. The definition quadVar S w = w ⬝ᵥ S *ᵥ w is the weight-covariance-weight variance functional for a finite linear estimator, and SphericalErrors S σ records the scalar-identity covariance condition S = σ² • I.

The main reusable facts are quadVar_nonneg, nonnegativity under a positive-semidefinite covariance matrix, and quadVar_spherical, the reduction quadVar S w = σ² * (w ⬝ᵥ w) under spherical errors. The probability-theoretic bridge to actual random variables is in GaussMarkov/Variance.lean; the least-variance ordering theorems are in GaussMarkov/LeastNorm.lean.

def quadVar reviewed

Causalean.GaussMarkov

This is the covariance quadratic form that gives the variance of a linear estimator.

Definition (Lean source)

def quadVar (S : Matrix Obs Obs ℝ) (w : Obs → ℝ) : ℝ := w ⬝ᵥ S *ᵥ w

Causalean.GaussMarkov.quadVar · Causalean/Estimation/GaussMarkov/QuadForm.lean:46

def SphericalErrors reviewed

Causalean.GaussMarkov

This condition says the covariance matrix has homoskedastic uncorrelated errors.

Definition (Lean source)

def SphericalErrors (S : Matrix Obs Obs ℝ) (σ : ℝ) : Prop := S = σ ^ 2 • (1 : Matrix Obs Obs ℝ)

Causalean.GaussMarkov.SphericalErrors · Causalean/Estimation/GaussMarkov/QuadForm.lean:66

lemma quadVar_spherical reviewed

Causalean.GaussMarkov

Under spherical errors, i.e. when the error covariance matrix S equals σ² times the identity, the linear-estimator variance functional at weight vector w reduces to the common variance σ² times the squared Euclidean length of w.

Formal statement

hypotheses

S :

Matrix Obs Obs ℝ

σ :

ℝ

h :

SphericalErrors S σ

w :

Obs → ℝ

conclusion

quadVar S w = σ ^ 2 * (w ⬝ᵥ w)

Proof (Lean source)

lemma quadVar_spherical {S : Matrix Obs Obs ℝ} {σ : ℝ} (h : SphericalErrors S σ) (w : Obs → ℝ) : quadVar S w = σ ^ 2 * (w ⬝ᵥ w) := by subst h rw [quadVar, smul_mulVec, one_mulVec, dotProduct_smul, smul_eq_mul]

Causalean.GaussMarkov.quadVar_spherical · Causalean/Estimation/GaussMarkov/QuadForm.lean:70 · uses SphericalErrors , quadVar

2 supporting declarations (lemmas, instances)

quadVar_def lemma — The quadratic variance form unfolds to the weight-covariance-weight product.

hypotheses

S :

Matrix Obs Obs ℝ

w :

Obs → ℝ

conclusion

quadVar S w = w ⬝ᵥ S *ᵥ w

Proof (Lean source)

lemma quadVar_def (S : Matrix Obs Obs ℝ) (w : Obs → ℝ) : quadVar S w = w ⬝ᵥ S *ᵥ w := rfl

Causalean.GaussMarkov.quadVar_def · Causalean/Estimation/GaussMarkov/QuadForm.lean:53
quadVar_nonneg lemma — A positive-semidefinite covariance matrix gives a nonnegative variance for every linear weight.

hypotheses

S :

Matrix Obs Obs ℝ

hS :

S.PosSemidef

w :

Obs → ℝ

conclusion

0 ≤ quadVar S w

Proof (Lean source)

lemma quadVar_nonneg {S : Matrix Obs Obs ℝ} (hS : S.PosSemidef) (w : Obs → ℝ) : 0 ≤ quadVar S w := by have h := hS.dotProduct_mulVec_nonneg w simpa [quadVar] using h

Causalean.GaussMarkov.quadVar_nonneg · Causalean/Estimation/GaussMarkov/QuadForm.lean:57

Variance 3 core · 1 supporting This file connects the deterministic Gauss-Markov quadratic form to the probability theory of finite random families. ★ variance_linearCombination

Variance Bridge

This file connects the deterministic Gauss-Markov quadratic form to the probability theory of finite random families. It defines covMatrix Y μ, the covariance matrix of the observations Y i, and proves variance_linearCombination: the variance of ∑ i, w i * Y i is exactly quadVar (covMatrix Y μ) w.

It also defines SphericalFamily, the probabilistic condition that all cells have variance σ² and distinct cells are uncorrelated, and proves sphericalFamily_covMatrix, which turns that condition into the deterministic SphericalErrors hypothesis used by the Gauss-Markov ordering theorems.

def covMatrix reviewed

Causalean.GaussMarkov

Covariance matrix of a finite family of random variables Y i.

Definition (Lean source)

noncomputable def covMatrix (Y : Obs → Ω → ℝ) (μ : Measure Ω) : Matrix Obs Obs ℝ := fun i j => cov[Y i, Y j; μ]

Causalean.GaussMarkov.covMatrix · Causalean/Estimation/GaussMarkov/Variance.lean:37

theorem variance_linearCombination reviewed

Causalean.GaussMarkov

Variance of a linear combination = covariance quadratic form. For a finite family of random variables Y i, each square-integrable, and any weight vector w, the variance of the random linear combination ∑ i, w i * Y i equals the quadratic form wᵀ Σ w, where Σ is the family's covariance matrix.

Formal statement

hypotheses

IsProbabilityMeasure μ

Y :

Obs → Ω → ℝ

hY :

∀ i, MemLp (Y i) 2 μ

w :

Obs → ℝ

conclusion

Var[fun ω => ∑ i, w i * Y i ω; μ] = quadVar (covMatrix Y μ) w

Proof (Lean source)

theorem variance_linearCombination [IsProbabilityMeasure μ] (Y : Obs → Ω → ℝ) (hY : ∀ i, MemLp (Y i) 2 μ) (w : Obs → ℝ) : Var[fun ω => ∑ i, w i * Y i ω; μ] = quadVar (covMatrix Y μ) w := by set X : Obs → Ω → ℝ := fun i ω => w i * Y i ω with hX_def have hX : ∀ i, MemLp (X i) 2 μ := fun i => (hY i).const_mul (w i) have hfun : (∑ i, X i) = fun ω => ∑ i, X i ω := by funext ω; exact Finset.sum_apply ω Finset.univ X have hSumMemLp : MemLp (fun ω => ∑ i, X i ω) 2 μ := by rw [← hfun] exact memLp_finset_sum' (μ := μ) (p := 2) Finset.univ (fun i (_ : i ∈ Finset.univ) => hX i) have hSum : AEMeasurable (fun ω => ∑ i, X i ω) μ := hSumMemLp.aestronglyMeasurable.aemeasurable calc Var[fun ω => ∑ i, w i * Y i ω; μ] = cov[fun ω => ∑ i, X i ω, fun ω => ∑ i, X i ω; μ] := (covariance_self hSum).symm _ = ∑ i, ∑ j, cov[X i, X j; μ] := covariance_fun_sum_fun_sum hX hX _ = ∑ i, ∑ j, w i * (w j * covMatrix Y μ i j) := by refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_)) rw [hX_def] rw [covariance_const_mul_left, covariance_const_mul_right] rfl _ = quadVar (covMatrix Y μ) w := by simp only [quadVar, dotProduct, mulVec, Finset.mul_sum] refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_)) ring

Causalean.GaussMarkov.variance_linearCombination · Causalean/Estimation/GaussMarkov/Variance.lean:41 · uses covMatrix , quadVar

def SphericalFamily reviewed

Causalean.GaussMarkov

A random family has spherical errors with scale σ: distinct cells are uncorrelated and each has variance σ².

Definition (Lean source)

def SphericalFamily (Y : Obs → Ω → ℝ) (μ : Measure Ω) (σ : ℝ) : Prop := (∀ i, Var[Y i; μ] = σ ^ 2) ∧ (∀ i j, i ≠ j → cov[Y i, Y j; μ] = 0)

Causalean.GaussMarkov.SphericalFamily · Causalean/Estimation/GaussMarkov/Variance.lean:71

1 supporting declaration (lemmas, instances)

sphericalFamily_covMatrix lemma — A spherical random family has a spherical (scalar-identity) covariance matrix.

hypotheses

DecidableEq Obs

Y :

Obs → Ω → ℝ

σ :

ℝ

hY :

∀ i, AEMeasurable (Y i) μ

h :

SphericalFamily Y μ σ

conclusion

SphericalErrors (covMatrix Y μ) σ

Proof (Lean source)

lemma sphericalFamily_covMatrix [DecidableEq Obs] {Y : Obs → Ω → ℝ} {σ : ℝ} (hY : ∀ i, AEMeasurable (Y i) μ) (h : SphericalFamily Y μ σ) : SphericalErrors (covMatrix Y μ) σ := by ext i j simp only [covMatrix, Matrix.smul_apply, Matrix.one_apply, smul_eq_mul] by_cases hij : i = j · subst hij rw [covariance_self (hY i), h.1 i] simp · rw [h.2 i j hij] simp [hij]

Causalean.GaussMarkov.sphericalFamily_covMatrix · Causalean/Estimation/GaussMarkov/Variance.lean:77

BLUE 2 core · 1 supporting This file states the finite Gauss-Markov conclusions in probabilistic variance language. ★ variance_blue_spherical★ variance_blue_gls

Best Linear Unbiased Estimation

This file states the finite Gauss-Markov conclusions in probabilistic variance language. It combines the covariance-matrix bridge with the least-norm ordering theorems to prove the best-linear-unbiased-estimator results for spherical errors and for a known covariance matrix.

theorem variance_blue_spherical reviewed

Causalean.GaussMarkov

BLUE under spherical errors (variance form). For a finite family of random variables Y i, each square-integrable, suppose the family is spherical: distinct cells are uncorrelated and every cell has the same variance σ². Among all linear combinations ∑ i, w i * Y i whose weights satisfy the same unbiasedness constraint w ᵥ* X = c relative to a design X and target combination c, if wStar lies in the column span of X, wStar = X *ᵥ g, then the linear combination built from wStar (the OLS weight) has variance no larger than that of any other unbiased linear combination.

Formal statement

hypotheses

IsProbabilityMeasure μ

X :

Matrix Obs Param ℝ

c :

Param → ℝ

Y :

Obs → Ω → ℝ

hY :

∀ i, MemLp (Y i) 2 μ

σ :

ℝ

hsph :

SphericalFamily Y μ σ

w wStar :

Obs → ℝ

g :

Param → ℝ

hStar :

wStar = X *ᵥ g

hUStar :

wStar ᵥ* X = c

hU :

w ᵥ* X = c

conclusion

Var[fun ω => ∑ i, wStar i * Y i ω; μ] ≤ Var[fun ω => ∑ i, w i * Y i ω; μ]

Proof (Lean source)

theorem variance_blue_spherical [IsProbabilityMeasure μ] {X : Matrix Obs Param ℝ} {c : Param → ℝ} (Y : Obs → Ω → ℝ) (hY : ∀ i, MemLp (Y i) 2 μ) {σ : ℝ} (hsph : SphericalFamily Y μ σ) {w wStar : Obs → ℝ} {g : Param → ℝ} (hStar : wStar = X *ᵥ g) (hUStar : wStar ᵥ* X = c) (hU : w ᵥ* X = c) : Var[fun ω => ∑ i, wStar i * Y i ω; μ] ≤ Var[fun ω => ∑ i, w i * Y i ω; μ] := by classical rw [variance_linearCombination Y hY, variance_linearCombination Y hY] have hsph' : SphericalErrors (covMatrix Y μ) σ := sphericalFamily_covMatrix (fun i => (hY i).aestronglyMeasurable.aemeasurable) hsph exact gauss_markov_spherical hsph' hStar hUStar hU

Causalean.GaussMarkov.variance_blue_spherical · Causalean/Estimation/GaussMarkov/BLUE.lean:57 · uses SphericalFamily

theorem variance_blue_gls reviewed

Causalean.GaussMarkov

BLUE for known covariance (GLS, variance form). For a finite family of random variables Y i, each square-integrable, consider linear combinations ∑ i, w i * Y i whose weights satisfy the same unbiasedness constraint w ᵥ* X = c relative to a design X and target combination c. If the weight wStar is a generalized-least-squares (GLS) weight — i.e. the family's covariance matrix applied to wStar lies in the column span of X, then the linear combination built from wStar has variance no larger than that of any other unbiased linear combination.

Formal statement

hypotheses

IsProbabilityMeasure μ

X :

Matrix Obs Param ℝ

c :

Param → ℝ

Y :

Obs → Ω → ℝ

hY :

∀ i, MemLp (Y i) 2 μ

w wStar :

Obs → ℝ

g :

Param → ℝ

hGLS :

(covMatrix Y μ) *ᵥ wStar = X *ᵥ g

hUStar :

wStar ᵥ* X = c

hU :

w ᵥ* X = c

conclusion

Var[fun ω => ∑ i, wStar i * Y i ω; μ] ≤ Var[fun ω => ∑ i, w i * Y i ω; μ]

Proof (Lean source)

theorem variance_blue_gls [IsProbabilityMeasure μ] {X : Matrix Obs Param ℝ} {c : Param → ℝ} (Y : Obs → Ω → ℝ) (hY : ∀ i, MemLp (Y i) 2 μ) {w wStar : Obs → ℝ} {g : Param → ℝ} (hGLS : (covMatrix Y μ) *ᵥ wStar = X *ᵥ g) (hUStar : wStar ᵥ* X = c) (hU : w ᵥ* X = c) : Var[fun ω => ∑ i, wStar i * Y i ω; μ] ≤ Var[fun ω => ∑ i, w i * Y i ω; μ] := by rw [variance_linearCombination Y hY, variance_linearCombination Y hY] exact gauss_markov_gls (covMatrix_posSemidef Y hY) hGLS hUStar hU

Causalean.GaussMarkov.variance_blue_gls · Causalean/Estimation/GaussMarkov/BLUE.lean:79 · uses covMatrix

1 supporting declaration (lemmas, instances)

covMatrix_posSemidef lemma — A covariance matrix of an L² random family is positive semidefinite: it is symmetric (cov is symmetric) and its quadratic form is a genuine variance, hence nonnegative. (Fintype Obs appears only under the PosSemidef definition, which the unusedFintypeInType linter cannot see; it is genuinely required.)

hypotheses

IsProbabilityMeasure μ

Y :

Obs → Ω → ℝ

hY :

∀ i, MemLp (Y i) 2 μ

conclusion

(covMatrix Y μ).PosSemidef

Proof (Lean source)

lemma covMatrix_posSemidef [IsProbabilityMeasure μ] (Y : Obs → Ω → ℝ) (hY : ∀ i, MemLp (Y i) 2 μ) : (covMatrix Y μ).PosSemidef := by refine Matrix.PosSemidef.of_dotProduct_mulVec_nonneg ?_ ?_ · refine Matrix.IsHermitian.ext fun i j => ?_ change star (covMatrix Y μ j i) = covMatrix Y μ i j rw [star_trivial] exact covariance_comm (Y j) (Y i) · intro w have hsw : star w ⬝ᵥ (covMatrix Y μ) *ᵥ w = quadVar (covMatrix Y μ) w := by simp [quadVar, star_trivial] rw [hsw, ← variance_linearCombination Y hY] exact variance_nonneg _ _

Causalean.GaussMarkov.covMatrix_posSemidef · Causalean/Estimation/GaussMarkov/BLUE.lean:37

LeastNorm 2 core · 2 supporting This file proves the algebraic core of the finite Gauss-Markov theorem. ★ gauss_markov_spherical★ gauss_markov_gls

Least-Norm Gauss-Markov Ordering

This file proves the algebraic core of the finite Gauss-Markov theorem. It shows that, among linear-estimator weights satisfying the same unbiasedness constraint w ᵥ* X = c, an ordinary least-squares weight in the column span of X is variance-minimizing under spherical errors and a generalized least-squares weight is variance-minimizing under a known positive-semidefinite covariance matrix.

The main public results are gauss_markov_spherical, the finite BLUE ordering for spherical covariance Σ = σ² I, and gauss_markov_gls, the corresponding ordering for a general positive-semidefinite covariance. The supporting lemma colSpan_dotProduct_leftNull records the orthogonality between the column span of X and the left null space that drives the Pythagorean variance comparison.

theorem gauss_markov_spherical reviewed

Causalean.GaussMarkov

Finite Gauss-Markov theorem, spherical case. Fix a design matrix X, a target combination c, and suppose the covariance matrix S is spherical: S = σ² I for some scale σ. Among all weight vectors w satisfying the same unbiasedness constraint w ᵥ* X = c, if wStar lies in the column span of X, wStar = X *ᵥ g, then the quadratic form wStarᵀ S wStar is no larger than wᵀ S w.

Formal statement

hypotheses

DecidableEq Obs

X :

Matrix Obs Param ℝ

c :

Param → ℝ

S :

Matrix Obs Obs ℝ

σ :

ℝ

hS :

SphericalErrors S σ

w wStar :

Obs → ℝ

g :

Param → ℝ

hStar :

wStar = X *ᵥ g

hUStar :

wStar ᵥ* X = c

hU :

w ᵥ* X = c

conclusion

quadVar S wStar ≤ quadVar S w

Proof (Lean source)

theorem gauss_markov_spherical [DecidableEq Obs] {X : Matrix Obs Param ℝ} {c : Param → ℝ} {S : Matrix Obs Obs ℝ} {σ : ℝ} (hS : SphericalErrors S σ) {w wStar : Obs → ℝ} {g : Param → ℝ} (hStar : wStar = X *ᵥ g) (hUStar : wStar ᵥ* X = c) (hU : w ᵥ* X = c) : quadVar S wStar ≤ quadVar S w := by -- `z := w - wStar` lies in the left null space of `X`. have hz : (w - wStar) ᵥ* X = 0 := by rw [sub_vecMul, hU, hUStar, sub_self] -- The OLS weight is orthogonal to `z` (it lies in the column span of `X`). have hortho : wStar ⬝ᵥ (w - wStar) = 0 := by have h := colSpan_dotProduct_leftNull (g := g) hz rwa [← hStar] at h -- Pythagoras: `‖w - wStar‖² = ‖w‖² - ‖wStar‖²`. have hcomm : w ⬝ᵥ wStar = wStar ⬝ᵥ w := dotProduct_comm w wStar have hcross : wStar ⬝ᵥ w = wStar ⬝ᵥ wStar := by have h := hortho; rw [dotProduct_sub] at h; linarith have key : (w - wStar) ⬝ᵥ (w - wStar) = w ⬝ᵥ w - wStar ⬝ᵥ wStar := by rw [sub_dotProduct, dotProduct_sub, dotProduct_sub] linarith have hznn := dotProduct_self_nonneg' (w - wStar) have hle : wStar ⬝ᵥ wStar ≤ w ⬝ᵥ w := by linarith rw [quadVar_spherical hS, quadVar_spherical hS] exact mul_le_mul_of_nonneg_left hle (sq_nonneg σ)

Causalean.GaussMarkov.gauss_markov_spherical · Causalean/Estimation/GaussMarkov/LeastNorm.lean:63 · uses SphericalErrors , quadVar

theorem gauss_markov_gls reviewed

Causalean.GaussMarkov

Finite Gauss-Markov theorem, general covariance (GLS). Fix a design matrix X, a target combination c, and a positive-semidefinite covariance matrix S. Among all weight vectors w satisfying the same unbiasedness constraint w ᵥ* X = c, if wStar is a GLS weight — meaning S *ᵥ wStar lies in the column span of X, then the quadratic form wStarᵀ S wStar is no larger than wᵀ S w. Specializes to gauss_markov_spherical when S = σ² I.

Formal statement

hypotheses

X :

Matrix Obs Param ℝ

c :

Param → ℝ

S :

Matrix Obs Obs ℝ

hS :

S.PosSemidef

w wStar :

Obs → ℝ

g :

Param → ℝ

hGLS :

S *ᵥ wStar = X *ᵥ g

hUStar :

wStar ᵥ* X = c

hU :

w ᵥ* X = c

conclusion

quadVar S wStar ≤ quadVar S w

Proof (Lean source)

theorem gauss_markov_gls {X : Matrix Obs Param ℝ} {c : Param → ℝ} {S : Matrix Obs Obs ℝ} (hS : S.PosSemidef) {w wStar : Obs → ℝ} {g : Param → ℝ} (hGLS : S *ᵥ wStar = X *ᵥ g) (hUStar : wStar ᵥ* X = c) (hU : w ᵥ* X = c) : quadVar S wStar ≤ quadVar S w := by have hsymm : Sᵀ = S := by have h := hS.isHermitian.eq rwa [conjTranspose_eq_transpose_of_trivial] at h set z := w - wStar with hzdef have hz : z ᵥ* X = 0 := by rw [hzdef, sub_vecMul, hU, hUStar, sub_self] -- Both `Σ`-inner-product cross terms vanish. have term1 : z ⬝ᵥ S *ᵥ wStar = 0 := by rw [hGLS, dotProduct_mulVec, hz, zero_dotProduct] have term2 : wStar ⬝ᵥ S *ᵥ z = 0 := by rw [dotProduct_mulVec, ← hsymm, vecMul_transpose, hGLS] exact colSpan_dotProduct_leftNull hz have hwz : w = wStar + z := by rw [hzdef]; abel have hexpand : quadVar S w = quadVar S wStar + quadVar S z := by simp only [quadVar] rw [hwz, mulVec_add, dotProduct_add, add_dotProduct, add_dotProduct, term1, term2] ring rw [hexpand] have := quadVar_nonneg hS z linarith

Causalean.GaussMarkov.gauss_markov_gls · Causalean/Estimation/GaussMarkov/LeastNorm.lean:93 · uses quadVar

2 supporting declarations (lemmas, instances)

colSpan_dotProduct_leftNull lemma — Column span is Euclidean-orthogonal to the left null space: if z lies in the left null space of X (z ᵥ* X = 0), then any column-span vector X *ᵥ g is orthogonal to z.

hypotheses

X :

Matrix Obs Param ℝ

g :

Param → ℝ

z :

Obs → ℝ

hz :

z ᵥ* X = 0

conclusion

(X *ᵥ g) ⬝ᵥ z = 0

Proof (Lean source)

lemma colSpan_dotProduct_leftNull {X : Matrix Obs Param ℝ} {g : Param → ℝ} {z : Obs → ℝ} (hz : z ᵥ* X = 0) : (X *ᵥ g) ⬝ᵥ z = 0 := by rw [dotProduct_comm, dotProduct_mulVec, hz, zero_dotProduct]

Causalean.GaussMarkov.colSpan_dotProduct_leftNull · Causalean/Estimation/GaussMarkov/LeastNorm.lean:51
dotProduct_self_nonneg' lemma — Nonnegativity of the Euclidean self dot product.

hypotheses

v :

Obs → ℝ

conclusion

0 ≤ v ⬝ᵥ v

Proof (Lean source)

lemma dotProduct_self_nonneg' (v : Obs → ℝ) : 0 ≤ v ⬝ᵥ v := by rw [dotProduct] exact sum_nonneg fun i _ => mul_self_nonneg _

Causalean.GaussMarkov.dotProduct_self_nonneg' · Causalean/Estimation/GaussMarkov/LeastNorm.lean:58

OLS 2 core · 2 supporting This file defines the ordinary least-squares weight vector olsWeight X c for estimating a specified linear combination c'β from a finite design matrix X. ★ olsWeight_blue_spherical

Ordinary Least Squares Weights

This file defines the ordinary least-squares weight vector olsWeight X c for estimating a specified linear combination c'β from a finite design matrix X. The definition uses the ordinary inverse of the normal-equations matrix Xᵀ * X; the unbiasedness theorem therefore assumes IsUnit (Xᵀ * X).det, the finite full-column-rank condition.

The public facts are olsWeight_unbiased, which proves the constraint olsWeight X c ᵥ* X = c, and olsWeight_blue_spherical, which applies gauss_markov_spherical to show that this OLS weight is BLUE under spherical errors.

def olsWeight reviewed

Causalean.GaussMarkov

OLS weight via the normal-equations inverse: wStar = X (XᵀX)⁻¹ c.

Definition (Lean source)

noncomputable def olsWeight (X : Matrix Obs Param ℝ) (c : Param → ℝ) : Obs → ℝ := X *ᵥ ((Xᵀ * X)⁻¹ *ᵥ c)

Causalean.GaussMarkov.olsWeight · Causalean/Estimation/GaussMarkov/OLS.lean:36

theorem olsWeight_blue_spherical reviewed

Causalean.GaussMarkov

OLS is BLUE under spherical errors. For an invertible normal-equations matrix Xᵀ X — full column rank — the ordinary-least-squares weight olsWeight X c estimating the target combination c is well defined. Under spherical errors S = σ² I, among all weight vectors w satisfying the same unbiasedness constraint w ᵥ* X = c, the quadratic form at the OLS weight is no larger than at any other unbiased weight w.

Formal statement

hypotheses

DecidableEq Obs

X :

Matrix Obs Param ℝ

c :

Param → ℝ

h :

IsUnit (Xᵀ * X).det

S :

Matrix Obs Obs ℝ

σ :

ℝ

hS :

SphericalErrors S σ

w :

Obs → ℝ

hU :

w ᵥ* X = c

conclusion

quadVar S (olsWeight X c) ≤ quadVar S w

Proof (Lean source)

theorem olsWeight_blue_spherical [DecidableEq Obs] {X : Matrix Obs Param ℝ} (c : Param → ℝ) (h : IsUnit (Xᵀ * X).det) {S : Matrix Obs Obs ℝ} {σ : ℝ} (hS : SphericalErrors S σ) {w : Obs → ℝ} (hU : w ᵥ* X = c) : quadVar S (olsWeight X c) ≤ quadVar S w := gauss_markov_spherical hS (olsWeight_mem_colSpan X c) (olsWeight_unbiased c h) hU

Causalean.GaussMarkov.olsWeight_blue_spherical · Causalean/Estimation/GaussMarkov/OLS.lean:61 · uses SphericalErrors , olsWeight , quadVar

2 supporting declarations (lemmas, instances)

olsWeight_mem_colSpan lemma — The OLS weight lies in the column span of X.

hypotheses

X :

Matrix Obs Param ℝ

c :

Param → ℝ

conclusion

olsWeight X c = X *ᵥ ((Xᵀ * X)⁻¹ *ᵥ c)

Proof (Lean source)

lemma olsWeight_mem_colSpan (X : Matrix Obs Param ℝ) (c : Param → ℝ) : olsWeight X c = X *ᵥ ((Xᵀ * X)⁻¹ *ᵥ c) := rfl

Causalean.GaussMarkov.olsWeight_mem_colSpan · Causalean/Estimation/GaussMarkov/OLS.lean:44
olsWeight_unbiased lemma — The OLS weight satisfies the unbiasedness constraint wStar ᵥ* X = c, provided XᵀX is invertible (full column rank).

hypotheses

X :

Matrix Obs Param ℝ

c :

Param → ℝ

h :

IsUnit (Xᵀ * X).det

conclusion

olsWeight X c ᵥ* X = c

Proof (Lean source)

lemma olsWeight_unbiased {X : Matrix Obs Param ℝ} (c : Param → ℝ) (h : IsUnit (Xᵀ * X).det) : olsWeight X c ᵥ* X = c := by have h1 : ∀ g : Param → ℝ, (X *ᵥ g) ᵥ* X = (Xᵀ * X) *ᵥ g := by intro g rw [← mulVec_transpose, mulVec_mulVec] calc olsWeight X c ᵥ* X = (Xᵀ * X) *ᵥ ((Xᵀ * X)⁻¹ *ᵥ c) := by rw [olsWeight, h1] _ = ((Xᵀ * X) * (Xᵀ * X)⁻¹) *ᵥ c := by rw [mulVec_mulVec] _ = (1 : Matrix Param Param ℝ) *ᵥ c := by rw [mul_nonsing_inv (Xᵀ * X) h] _ = c := one_mulVec c

Causalean.GaussMarkov.olsWeight_unbiased · Causalean/Estimation/GaussMarkov/OLS.lean:48

Estimation.Gauss­Markov

Quadratic Variance Form

Variance Bridge

Best Linear Unbiased Estimation

Least-Norm Gauss-Markov Ordering

Ordinary Least Squares Weights

Estimation.GaussMarkov