Stat.Linear­Model.Gauss­Markov

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

Quad­Form 3 core · 2 supporting This file provides the deterministic layer for finite covariance quadratic-form comparisons. ★ quadVar_spherical

Quadratic Variance Form

This file provides the deterministic layer for finite covariance quadratic-form comparisons. 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 quadratic-form ordering theorems are in GaussMarkov/LeastNorm.lean.

def quadVar reviewed
Causalean.Stat.GaussMarkov

For a finite observation index set, a real covariance matrix indexed by that set, and a real weight assigned to each observation, the quadratic variance form is wTSww^\mathsf{T} S w.

Definition (Lean source)
parameters
Obs :
Type u_1
shared
S :
Matrix Obs Obs ℝ
w :
Obs → ℝ
def
quadVar S w :
ℝ
given by
w ⬝ᵥ S *ᵥ w
Causalean.Stat.GaussMarkov.quadVar · Causalean/Stat/LinearModel/GaussMarkov/QuadForm.lean:32
def SphericalErrors reviewed
Causalean.Stat.GaussMarkov

For an observation index set in which equality can be decided, a real square matrix indexed by those observations, and a real scale parameter, the spherical-errors condition holds exactly when the matrix equals σ2σ^2 times the identity matrix.

Definition (Lean source)
parameters
Obs :
Type u_1
shared
S :
Matrix Obs Obs ℝ
σ :
ℝ
def
SphericalErrors S σ :
Prop
given by
S = σ ^ 2 • (1 : Matrix Obs Obs ℝ)
Causalean.Stat.GaussMarkov.SphericalErrors · Causalean/Stat/LinearModel/GaussMarkov/QuadForm.lean:54
lemma quadVar_spherical reviewed
Causalean.Stat.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
Obs :
Type u_1
Matrix Obs Obs ℝ
shared
σ :
ℝ
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.Stat.GaussMarkov.quadVar_spherical · Causalean/Stat/LinearModel/GaussMarkov/QuadForm.lean:61 · uses SphericalErrors , quadVar
2 supporting declarations (lemmas, instances)
Variance 3 core · 1 supporting This file connects the deterministic covariance quadratic form to the probability theory of finite random families. ★ variance_linearCombination

Variance Bridge

This file connects the deterministic covariance 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 quadratic-form ordering theorems.

def covMatrix reviewed
Causalean.Stat.GaussMarkov

For a sample space equipped with a σ-algebra, a finite observation index set, a real-valued random variable for each observation, and a measure on the sample space, the covariance matrix has entry (i,j)(i,j) equal to the covariance of the iith and jjth random variables under that measure.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
Obs :
Type u_2
shared
mΩ :
MeasurableSpace Ω
shared
Y :
Obs → Ω → ℝ
μ :
Measure Ω
def
covMatrix Y μ :
Matrix Obs Obs ℝ
given by
fun i j => cov[Y i, Y j; μ]
Causalean.Stat.GaussMarkov.covMatrix · Causalean/Stat/LinearModel/GaussMarkov/Variance.lean:33
theorem variance_linearCombination reviewed
Causalean.Stat.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
Ω :
Type u_1
shared
Obs :
Type u_2
shared
mΩ :
MeasurableSpace Ω
shared
μ :
Measure Ω
IsProbabilityMeasure μ
shared
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.Stat.GaussMarkov.variance_linearCombination · Causalean/Stat/LinearModel/GaussMarkov/Variance.lean:41 · uses covMatrix , quadVar
def SphericalFamily reviewed
Causalean.Stat.GaussMarkov

For a sample space equipped with a σ-algebra, a finite observation index set, a real-valued random variable for each observation, a measure on the sample space, and a real scale parameter, the spherical-family condition holds exactly when every random variable has variance σ2σ^2 and every two indexed by distinct observations have covariance zero.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
Obs :
Type u_2
shared
mΩ :
MeasurableSpace Ω
shared
Y :
Obs → Ω → ℝ
μ :
Measure Ω
σ :
ℝ
def
SphericalFamily Y μ σ :
Prop
given by
clause 1
i :
Var[Y i; μ] = σ ^ 2
clause 2
i j :
i ≠ j
cov[Y i, Y j; μ] = 0
Causalean.Stat.GaussMarkov.SphericalFamily · Causalean/Stat/LinearModel/GaussMarkov/Variance.lean:71
1 supporting declaration (lemmas, instances)
BLUE 2 core · 1 supporting This file combines the covariance-matrix bridge with algebraic quadratic-form orderings to compare variances of finite random linear combinations. ★ linearCombination_variance_spherical_le_of_colSpan★ linearCombination_variance_le_of_covMul_mem_colSpan

Variance Orderings for Linear Combinations

This file combines the covariance-matrix bridge with algebraic quadratic-form orderings to compare variances of finite random linear combinations. The weights satisfy common design-balance identities, but the statements do not assume a linear mean model and therefore do not by themselves prove estimator unbiasedness.

theorem linearCombination_variance_spherical_le_of_colSpan reviewed
Causalean.Stat.GaussMarkov

Variance ordering under a spherical random family. 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 design-balance identity w ᵥ* X = c, if wStar lies in the column span of X, wStar = X *ᵥ g, then the linear combination built from wStar has variance no larger than the one built from w.

Formal statement
hypotheses
Ω :
Type u_1
shared
Obs :
Type u_2
shared
mΩ :
MeasurableSpace Ω
shared
μ :
Measure Ω
shared
Param :
Type u_3
shared
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 linearCombination_variance_spherical_le_of_colSpan [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 quadVar_spherical_le_of_colSpan hsph' hStar hUStar hU
Causalean.Stat.GaussMarkov.linearCombination_variance_spherical_le_of_colSpan · Causalean/Stat/LinearModel/GaussMarkov/BLUE.lean:49 · uses SphericalFamily
theorem linearCombination_variance_le_of_covMul_mem_colSpan reviewed
Causalean.Stat.GaussMarkov

Variance ordering under a known covariance matrix. 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 design-balance identity w ᵥ* X = c. If 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 the one built from w.

Formal statement
hypotheses
Ω :
Type u_1
shared
Obs :
Type u_2
shared
mΩ :
MeasurableSpace Ω
shared
μ :
Measure Ω
shared
Param :
Type u_3
shared
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 linearCombination_variance_le_of_covMul_mem_colSpan [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 quadVar_le_of_mulVec_mem_colSpan (covMatrix_posSemidef Y hY) hGLS hUStar hU
Causalean.Stat.GaussMarkov.linearCombination_variance_le_of_covMul_mem_colSpan · Causalean/Stat/LinearModel/GaussMarkov/BLUE.lean:70 · uses covMatrix
1 supporting declaration (lemmas, instances)
Least­Norm 2 core · 2 supporting This file proves algebraic quadratic-form orderings for weights satisfying the same design-balance identity w ᵥ* X = c. ★ quadVar_spherical_le_of_colSpan★ quadVar_le_of_mulVec_mem_colSpan

Least-Norm Covariance Ordering

This file proves algebraic quadratic-form orderings for weights satisfying the same design-balance identity w ᵥ* X = c. A column-span weight has no larger quadratic form under a spherical matrix, and a weight whose image under a positive-semidefinite matrix lies in the column span has no larger quadratic form under that matrix. The statements do not include a mean model and therefore do not themselves establish estimator unbiasedness.

The main public results are quadVar_spherical_le_of_colSpan and quadVar_le_of_mulVec_mem_colSpan. The supporting lemma colSpan_dotProduct_leftNull records the orthogonality between the column span of X and the left null space that drives the Pythagorean comparison.

theorem quadVar_spherical_le_of_colSpan reviewed
Causalean.Stat.GaussMarkov

Spherical quadratic-form ordering. Fix a design matrix X, a target combination c, and suppose the matrix S is spherical: S = σ² I for some scale σ. Among all weight vectors w satisfying the same design-balance identity 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
Obs :
Type u_1
shared
Param :
Type u_2
shared
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 quadVar_spherical_le_of_colSpan [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 column-span weight is orthogonal to `z`. 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.Stat.GaussMarkov.quadVar_spherical_le_of_colSpan · Causalean/Stat/LinearModel/GaussMarkov/LeastNorm.lean:44 · uses SphericalErrors , quadVar
theorem quadVar_le_of_mulVec_mem_colSpan reviewed
Causalean.Stat.GaussMarkov

Positive-semidefinite quadratic-form ordering. Fix a design matrix X, a target combination c, and a positive-semidefinite matrix S. Among all weight vectors w satisfying the same design-balance identity w ᵥ* X = c, if the image S *ᵥ wStar lies in the column span of X, then the quadratic form wStarᵀ S wStar is no larger than wᵀ S w.

Formal statement
hypotheses
Obs :
Type u_1
shared
Param :
Type u_2
Matrix Obs Param ℝ
Param → ℝ
shared
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 quadVar_le_of_mulVec_mem_colSpan {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.Stat.GaussMarkov.quadVar_le_of_mulVec_mem_colSpan · Causalean/Stat/LinearModel/GaussMarkov/LeastNorm.lean:75 · 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
    Obs :
    Type u_1
    shared
    Param :
    Type u_2
    Matrix Obs Param ℝ
    Param → ℝ
    shared
    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.Stat.GaussMarkov.colSpan_dotProduct_leftNull · Causalean/Stat/LinearModel/GaussMarkov/LeastNorm.lean:32
  • dotProduct_self_nonneg' lemma — Nonnegativity of the Euclidean self dot product.
    hypotheses
    Obs :
    Type u_1
    shared
    v :
    Obs → ℝ
    conclusion
    0 ≤ v ⬝ᵥ v
    Proof (Lean source)
    lemma dotProduct_self_nonneg' (v : Obs → ℝ) : 0 ≤ v ⬝ᵥ v := by rw [dotProduct] exact Finset.sum_nonneg fun i _ => mul_self_nonneg _
    Causalean.Stat.GaussMarkov.dotProduct_self_nonneg' · Causalean/Stat/LinearModel/GaussMarkov/LeastNorm.lean:39
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_quadVar_spherical_le

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 design-balance identity therefore assumes IsUnit (Xᵀ * X).det, the finite full-column-rank condition.

The public facts are olsWeight_vecMul_eq, which proves olsWeight X c ᵥ* X = c, and olsWeight_quadVar_spherical_le, which applies quadVar_spherical_le_of_colSpan to compare the OLS weight's quadratic form with every weight satisfying the same identity. These facts alone do not prove unbiasedness because they do not include a mean model.

def olsWeight reviewed
Causalean.Stat.GaussMarkov

For finite observation and parameter index sets, with parameter indices that can be distinguished, a real design matrix, and a real vector specifying a linear combination of the parameters, the ordinary-least-squares weight vector is X(XTX)−1cX(X^\mathsf{T}X)^{-1}c.

Definition (Lean source)
parameters
Obs :
Type u_1
shared
Param :
Type u_2
shared
X :
Matrix Obs Param ℝ
c :
Param → ℝ
def
olsWeight X c :
Obs → ℝ
given by
X *ᵥ ((Xᵀ * X)⁻¹ *ᵥ c)
Causalean.Stat.GaussMarkov.olsWeight · Causalean/Stat/LinearModel/GaussMarkov/OLS.lean:32
theorem olsWeight_quadVar_spherical_le reviewed
Causalean.Stat.GaussMarkov

OLS-weight quadratic-form ordering under a spherical matrix. For an invertible normal-equations matrix Xᵀ X and a spherical matrix S = σ² I, among all weight vectors w satisfying the same design-balance identity w ᵥ* X = c, the quadratic form at olsWeight X c is no larger than at w.

Formal statement
hypotheses
Obs :
Type u_1
shared
Param :
Type u_2
shared
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_quadVar_spherical_le [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 := quadVar_spherical_le_of_colSpan hS (olsWeight_mem_colSpan X c) (olsWeight_vecMul_eq c h) hU
Causalean.Stat.GaussMarkov.olsWeight_quadVar_spherical_le · Causalean/Stat/LinearModel/GaussMarkov/OLS.lean:60 · uses SphericalErrors , olsWeight , quadVar
2 supporting declarations (lemmas, instances)
  • olsWeight_mem_colSpan lemma — The OLS weight lies in the column span of X.
    hypotheses
    Obs :
    Type u_1
    shared
    Param :
    Type u_2
    shared
    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.Stat.GaussMarkov.olsWeight_mem_colSpan · Causalean/Stat/LinearModel/GaussMarkov/OLS.lean:43
  • olsWeight_vecMul_eq lemma — For an invertible normal-equations matrix XᵀX, the OLS weight satisfies the design-balance identity olsWeight X c ᵥ* X = c.
    hypotheses
    Obs :
    Type u_1
    shared
    Param :
    Type u_2
    Matrix Obs Param ℝ
    shared
    c :
    Param → ℝ
    h :
    IsUnit (Xᵀ * X).det
    conclusion
    olsWeight X c ᵥ* X = c
    Proof (Lean source)
    lemma olsWeight_vecMul_eq {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.Stat.GaussMarkov.olsWeight_vecMul_eq · Causalean/Stat/LinearModel/GaussMarkov/OLS.lean:47