Mathlib.Analysis.InnerProductSpace

InnerProductSpace — Mathlib-shaped helpers: FrischWaughLovell, Gram, Projection, RKHS.

PosDef 6 core · 9 supporting · 1 submodule PosDef — Mathlib-shaped helpers: Sqrt.

FrischWaughLovell 10 core · 18 supporting This file formalizes the finite-dimensional Frisch--Waugh--Lovell residualization theorem on a real inner-product space with a nuisance subspace admitting an orthogonal projection. ★ fwlCoef_original_minimizes★ original_minimizer_eq_fwlCoef_projection

Frisch-Waugh-Lovell Algebra

This file formalizes the finite-dimensional Frisch--Waugh--Lovell residualization theorem on a real inner-product space with a nuisance subspace admitting an orthogonal projection. It is a causal-agnostic linear-algebra layer: downstream estimand-characterization modules instantiate this result, but the statements here only mention inner products, finite regressor tuples, Gram matrices, and least-squares objectives.

Main definitions: * residualize H v is the orthogonal residual v - P_H v. * fittedValue X β is the finite linear combination of regressors X. * gramResid H X is the Gram matrix of the residualized regressors. * residInnerVec H X Y is the right-hand side of the residualized normal equations. * fwlCoef H X Y is the coefficient vector obtained by multiplying that right-hand side by the nonsingular inverse of gramResid H X. * residualizedObjective and originalObjective are the least-squares objectives after residualization and before residualizing out the nuisance term.

Main results: * residualize_inner_swap_right shows that the outcome can be residualized in inner products against a residualized regressor. * gramResid_mulVec_fwlCoef gives the residualized normal equations. * fwlCoef_residualized_minimizes proves that fwlCoef minimizes the residualized objective. * fwlCoef_original_minimizes lifts that optimizer to the original objective with an explicit nuisance term in H. * fwlCoef_eq_of_original_minimizer and original_minimizer_eq_fwlCoef_projection give the coefficient and full optimizer uniqueness characterizations.

def residualize reviewed

Causalean.Mathlib.FWL

For a real inner-product space, a subspace that admits an orthogonal projection, and a vector, the orthogonal residual is the vector minus its orthogonal projection onto that subspace.

Definition (Lean source)

parameters

V :

Type u_1

shared

H :

Submodule ℝ V

shared

v :

def

residualize H v :

given by

v - H.orthogonalProjectionFn v

Causalean.Mathlib.FWL.residualize · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:96

def residualizeL reviewed

Causalean.Mathlib.FWL

For a real inner-product space and a subspace that admits an orthogonal projection, the residual-maker linear map sends each vector to its orthogonal residual after removal of its projection onto that subspace.

Definition (Lean source)

parameters

V :

Type u_1

shared

H :

Submodule ℝ V

shared

def

residualizeL H :

V →L[ℝ] V

given by

id ℝ V - H.starProjection

Causalean.Mathlib.FWL.residualizeL · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:109

def fittedValue reviewed

Causalean.Mathlib.FWL

For a real inner-product space, a finite number of regressors, a tuple of regressor vectors, and a vector of real coefficients, the fitted value is the sum of each regressor multiplied by its corresponding coefficient.

Definition (Lean source)

parameters

V :

Type u_1

shared

K :

ℕ

shared

X :

Fin K → V

shared

β :

Fin K → ℝ

def

fittedValue X β :

given by

∑ j, β j • X j

Causalean.Mathlib.FWL.fittedValue · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:156

def gramResid reviewed

Causalean.Mathlib.FWL

For a real inner-product space, a subspace that admits an orthogonal projection, a finite number of regressors, and a tuple of regressor vectors, the residualized Gram matrix has as its $(j,k)$ entry the inner product of the orthogonal residuals of the $j$ th and $k$ th regressors.

Definition (Lean source)

parameters

V :

Type u_1

shared

H :

Submodule ℝ V

shared

K :

ℕ

shared

X :

Fin K → V

shared

def

gramResid H X :

Matrix (Fin K) (Fin K) ℝ

given by

fun j k => inner ℝ (residualize H (X j)) (residualize H (X k))

Causalean.Mathlib.FWL.gramResid · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:190

def residInnerVec reviewed

Causalean.Mathlib.FWL

For a real inner-product space, a subspace that admits an orthogonal projection, a finite number of regressors, a tuple of regressor vectors, and an outcome vector, the residualized inner-product vector assigns to each regressor index the inner product of that regressor's orthogonal residual with the outcome.

Definition (Lean source)

parameters

V :

Type u_1

shared

H :

Submodule ℝ V

shared

K :

ℕ

shared

X :

Fin K → V

shared

Y :

def

residInnerVec H X Y :

Fin K → ℝ

given by

fun j => inner ℝ (residualize H (X j)) Y

Causalean.Mathlib.FWL.residInnerVec · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:203

def fwlCoef reviewed

Causalean.Mathlib.FWL

For a real inner-product space, a subspace that admits an orthogonal projection, a finite number of regressors, a tuple of regressor vectors, and an outcome vector, the Frisch–Waugh–Lovell coefficient vector is the inverse residualized Gram matrix multiplied by the vector of inner products between residualized regressors and the outcome.

Definition (Lean source)

parameters

V :

Type u_1

shared

H :

Submodule ℝ V

shared

K :

ℕ

shared

X :

Fin K → V

shared

Y :

def

fwlCoef H X Y :

Fin K → ℝ

given by

(gramResid H X)⁻¹.mulVec (residInnerVec H X Y)

Causalean.Mathlib.FWL.fwlCoef · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:215

def residualizedObjective reviewed

Causalean.Mathlib.FWL

For a real inner-product space, a subspace that admits an orthogonal projection, a finite number of regressors, a tuple of regressor vectors, an outcome vector, and a vector of real coefficients, the residualized least-squares objective is the squared norm of the orthogonal residual of the outcome minus the fitted value formed from the orthogonal residuals of the regressors.

Definition (Lean source)

parameters

V :

Type u_1

shared

H :

Submodule ℝ V

shared

K :

ℕ

shared

X :

Fin K → V

shared

Y :

β :

Fin K → ℝ

def

residualizedObjective H X Y β :

ℝ

given by

inner ℝ (residualize H Y - fittedValue (fun j => residualize H (X j)) β) (residualize H Y - fittedValue (fun j => residualize H (X j)) β)

Causalean.Mathlib.FWL.residualizedObjective · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:245

def originalObjective reviewed

Causalean.Mathlib.FWL

For a real inner-product space, a finite number of regressors, a tuple of regressor vectors, an outcome vector, a vector of real coefficients, and a nuisance vector, the original least-squares objective is the squared norm of the outcome minus its fitted value and minus the nuisance vector.

Definition (Lean source)

parameters

V :

Type u_1

shared

K :

ℕ

shared

X :

Fin K → V

shared

Y :

β :

Fin K → ℝ

h :

def

originalObjective X Y β h :

ℝ

given by

inner ℝ (Y - fittedValue X β - h) (Y - fittedValue X β - h)

Causalean.Mathlib.FWL.originalObjective · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:255

theorem fwlCoef_original_minimizes reviewed

Causalean.Mathlib.FWL

Standard finite-dimensional Frisch–Waugh–Lovell theorem. On a real inner-product space with a nuisance subspace H admitting an orthogonal projection, and a finite tuple of regressors X, if the residualized Gram matrix of X has nonzero determinant, i.e. is invertible and a candidate nuisance vector h lies in H, then the original least-squares objective — evaluated at the FWL coefficient together with the orthogonal-projection nuisance term of its raw residual — is at most the original objective at any other coefficient vector β and nuisance term h.

Formal statement

hypotheses

V :

Type u_1

shared

H :

Submodule ℝ V

shared

K :

ℕ

shared

X :

Fin K → V

shared

Y :

hQ :

IsUnit (gramResid H X).det

β :

Fin K → ℝ

h :

hh :

h ∈ H

conclusion

originalObjective X Y (fwlCoef H X Y) (H.orthogonalProjectionFn (Y - fittedValue X (fwlCoef H X Y)))

≤ originalObjective X Y β h

Proof (Lean source)

theorem fwlCoef_original_minimizes (Y : V) (hQ : IsUnit (gramResid H X).det) (β : Fin K → ℝ) {h : V} (hh : h ∈ H) : originalObjective X Y (fwlCoef H X Y) (H.orthogonalProjectionFn (Y - fittedValue X (fwlCoef H X Y))) ≤ originalObjective X Y β h := by calc originalObjective X Y (fwlCoef H X Y) (H.orthogonalProjectionFn (Y - fittedValue X (fwlCoef H X Y))) = residualizedObjective H X Y (fwlCoef H X Y) := by rw [originalObjective_projection_eq_residualizedObjective] _ ≤ residualizedObjective H X Y β := fwlCoef_residualized_minimizes H X Y hQ β _ ≤ originalObjective X Y β h := residualizedObjective_le_originalObjective H X Y β hh

Causalean.Mathlib.FWL.fwlCoef_original_minimizes · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:403 · uses fittedValue , fwlCoef , gramResid , originalObjective

theorem original_minimizer_eq_fwlCoef_projection reviewed

Causalean.Mathlib.FWL

Uniqueness of the original least-squares minimizer. If the residualized Gram matrix of X is invertible, a candidate nuisance vector h lies in H, and the pair (β, h) minimizes the original least-squares objective over all coefficient vectors and nuisance terms in H, then β equals the FWL coefficient and h equals the orthogonal-projection nuisance term of the FWL coefficient's raw residual.

Formal statement

hypotheses

V :

Type u_1

shared

H :

Submodule ℝ V

shared

K :

ℕ

shared

X :

Fin K → V

shared

Y :

hQ :

IsUnit (gramResid H X).det

β :

Fin K → ℝ

h :

hh :

h ∈ H

hmin :

∀ (γ : Fin K → ℝ) {g : V}

g ∈ H

then

originalObjective X Y β h ≤ originalObjective X Y γ g

conclusion

conclusion 1

β = fwlCoef H X Y

conclusion 2

h = H.orthogonalProjectionFn (Y - fittedValue X (fwlCoef H X Y))

Proof (Lean source)

theorem original_minimizer_eq_fwlCoef_projection (Y : V) (hQ : IsUnit (gramResid H X).det) (β : Fin K → ℝ) {h : V} (hh : h ∈ H) (hmin : ∀ (γ : Fin K → ℝ) {g : V}, g ∈ H → originalObjective X Y β h ≤ originalObjective X Y γ g) : β = fwlCoef H X Y ∧ h = H.orthogonalProjectionFn (Y - fittedValue X (fwlCoef H X Y)) := by have hβ : β = fwlCoef H X Y := fwlCoef_eq_of_original_minimizer H X Y hQ β hh hmin have hp : h = H.orthogonalProjectionFn (Y - fittedValue X β) := by let p : V := H.orthogonalProjectionFn (Y - fittedValue X β) have hp_mem : p ∈ H := by dsimp [p] exact Submodule.starProjection_apply_mem H (Y - fittedValue X β) have hle : originalObjective X Y β h ≤ originalObjective X Y β p := hmin β hp_mem have hsplit := originalObjective_eq_residualizedObjective_add_projectionError H X Y β hh have hproj : originalObjective X Y β p = residualizedObjective H X Y β := by simpa [p] using originalObjective_projection_eq_residualizedObjective H X Y β rw [hsplit, hproj] at hle have hnonneg : 0 ≤ inner ℝ (H.orthogonalProjectionFn (Y - fittedValue X β) - h) (H.orthogonalProjectionFn (Y - fittedValue X β) - h) := by simp have hz : inner ℝ (H.orthogonalProjectionFn (Y - fittedValue X β) - h) (H.orthogonalProjectionFn (Y - fittedValue X β) - h) = 0 := by linarith have hzero : H.orthogonalProjectionFn (Y - fittedValue X β) - h = 0 := inner_self_eq_zero.mp hz rw [sub_eq_zero] at hzero exact hzero.symm constructor · exact hβ · rw [hp, hβ]

Causalean.Mathlib.FWL.original_minimizer_eq_fwlCoef_projection · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:477 · uses fittedValue , fwlCoef , gramResid , originalObjective

18 supporting declarations (lemmas, instances)

residualize_def lemma — Residualization is the original vector minus its orthogonal projection onto the nuisance subspace.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

v :

V

conclusion

residualize H v = v - H.orthogonalProjectionFn v

Proof (Lean source)

@[simp] lemma residualize_def (v : V) : residualize H v = v - H.orthogonalProjectionFn v := rfl

Causalean.Mathlib.FWL.residualize_def · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:104
residualizeL_apply lemma — Applying the residual-maker linear map gives the residualized vector.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

v :

V

conclusion

residualizeL H v = residualize H v

Proof (Lean source)

@[simp] lemma residualizeL_apply (v : V) : residualizeL H v = residualize H v := by simp [residualizeL, residualize]

Causalean.Mathlib.FWL.residualizeL_apply · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:117
inner_residualize_of_mem lemma — Residual is orthogonal to every element of H. This is the defining property of the orthogonal residual.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

v :

V

w :

V

hw :

w ∈ H

conclusion

inner ℝ (residualize H v) w = 0

Proof (Lean source)

lemma inner_residualize_of_mem (v : V) {w : V} (hw : w ∈ H) : inner ℝ (residualize H v) w = 0 := by simpa [residualize] using Submodule.orthogonalProjectionFn_inner_eq_zero (K := H) v w hw

Causalean.Mathlib.FWL.inner_residualize_of_mem · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:122
residualize_inner_swap_right lemma — Symmetric residualization in the right slot. Since M_H is self-adjoint and idempotent, ⟨X̃, Y⟩ = ⟨X̃, Ỹ⟩.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

v w :

V

conclusion

inner ℝ (residualize H v) w = inner ℝ (residualize H v) (residualize H w)

Proof (Lean source)

lemma residualize_inner_swap_right (v w : V) : inner ℝ (residualize H v) w = inner ℝ (residualize H v) (residualize H w) := by -- `w = residualize H w + P_H w` and `P_H w ∈ H`, which is orthogonal -- to `residualize H v`. have hPw : H.orthogonalProjectionFn w ∈ H := Submodule.starProjection_apply_mem H w have horth : inner ℝ (residualize H v) (H.orthogonalProjectionFn w) = 0 := inner_residualize_of_mem H v hPw have hsplit : w = residualize H w + H.orthogonalProjectionFn w := by simp [residualize, sub_add_cancel] calc inner ℝ (residualize H v) w = inner ℝ (residualize H v) (residualize H w + H.orthogonalProjectionFn w) := by rw [← hsplit] _ = inner ℝ (residualize H v) (residualize H w) + inner ℝ (residualize H v) (H.orthogonalProjectionFn w) := by rw [inner_add_right] _ = inner ℝ (residualize H v) (residualize H w) := by rw [horth, add_zero]

Causalean.Mathlib.FWL.residualize_inner_swap_right · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:130
fittedValue_sub lemma — Fitted values are linear in the coefficient vector.

hypotheses

V :

Type u_1
shared

K :

ℕ
shared

X :

Fin K → V
shared

β γ :

Fin K → ℝ

conclusion

fittedValue X (fun j => β j - γ j) = fittedValue X β - fittedValue X γ

Proof (Lean source)

lemma fittedValue_sub (β γ : Fin K → ℝ) : fittedValue X (fun j => β j - γ j) = fittedValue X β - fittedValue X γ := by simp [fittedValue, sub_smul, Finset.sum_sub_distrib]

Causalean.Mathlib.FWL.fittedValue_sub · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:162
residualize_fittedValue lemma — Residualization commutes with forming a fitted value.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

β :

Fin K → ℝ

conclusion

residualize H (fittedValue X β) = fittedValue (fun j => residualize H (X j)) β

Proof (Lean source)

lemma residualize_fittedValue (β : Fin K → ℝ) : residualize H (fittedValue X β) = fittedValue (fun j => residualize H (X j)) β := by rw [← residualizeL_apply] change residualizeL H (fittedValue X β) = fittedValue (fun j => residualizeL H (X j)) β simp [fittedValue]

Causalean.Mathlib.FWL.residualize_fittedValue · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:168
residualize_regressionResidual lemma — Residualization of the raw regression residual is the residualized outcome minus the fitted value of the residualized regressors.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

Y :

V

β :

Fin K → ℝ

conclusion

residualize H (Y - fittedValue X β)
= residualize H Y - fittedValue (fun j => residualize H (X j)) β

Proof (Lean source)

lemma residualize_regressionResidual (Y : V) (β : Fin K → ℝ) : residualize H (Y - fittedValue X β) = residualize H Y - fittedValue (fun j => residualize H (X j)) β := by rw [← residualizeL_apply] change residualizeL H (Y - fittedValue X β) = residualizeL H Y - fittedValue (fun j => residualizeL H (X j)) β rw [map_sub] rw [show residualizeL H (fittedValue X β) = fittedValue (fun j => residualizeL H (X j)) β by simpa [residualizeL_apply] using residualize_fittedValue H X β]

Causalean.Mathlib.FWL.residualize_regressionResidual · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:177
gramResid_apply lemma — Each entry of the residualized Gram matrix is the inner product of two residualized regressors.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

j k :

Fin K

conclusion

gramResid H X j k = inner ℝ (residualize H (X j)) (residualize H (X k))

Proof (Lean source)

@[simp] lemma gramResid_apply (j k : Fin K) : gramResid H X j k = inner ℝ (residualize H (X j)) (residualize H (X k)) := rfl

Causalean.Mathlib.FWL.gramResid_apply · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:197
residInnerVec_apply lemma — Each entry of the residualized right-hand side is the inner product of a residualized regressor with the outcome.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

Y :

V

j :

Fin K

conclusion

residInnerVec H X Y j = inner ℝ (residualize H (X j)) Y

Proof (Lean source)

@[simp] lemma residInnerVec_apply (Y : V) (j : Fin K) : residInnerVec H X Y j = inner ℝ (residualize H (X j)) Y := rfl

Causalean.Mathlib.FWL.residInnerVec_apply · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:210
gramResid_mulVec_fwlCoef lemma — Residualized normal equations (FWL coefficient form). If Q_{XX} = gramResid H X is invertible (equivalently, the residualized regressors are linearly independent), the FWL coefficient fwlCoef H X Y = Q_{XX}⁻¹ *ᵥ (fun j => ⟨X̃ j, Y⟩) satisfies the residualized normal equations Q_{XX} *ᵥ fwlCoef H X Y = (fun j => ⟨X̃ j, Y⟩).

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

Y :

V

hQ :

IsUnit (gramResid H X).det

conclusion

(gramResid H X).mulVec (fwlCoef H X Y) = residInnerVec H X Y

Proof (Lean source)

lemma gramResid_mulVec_fwlCoef (Y : V) (hQ : IsUnit (gramResid H X).det) : (gramResid H X).mulVec (fwlCoef H X Y) = residInnerVec H X Y := by -- Pure matrix algebra: `A *ᵥ (A⁻¹ *ᵥ b) = b` when `A.det` is a unit. unfold fwlCoef rw [Matrix.mulVec_mulVec, Matrix.mul_nonsing_inv _ hQ, Matrix.one_mulVec]

Causalean.Mathlib.FWL.gramResid_mulVec_fwlCoef · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:223
residInnerVec_eq_residualize_right lemma — Symmetric residualization for the FWL right-hand side. The residualized inner products ⟨X̃ j, Y⟩ agree with ⟨X̃ j, Ỹ⟩, so the FWL coefficient depends only on the residualized response.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

Y :

V

conclusion

residInnerVec H X Y = residInnerVec H X (residualize H Y)

Proof (Lean source)

lemma residInnerVec_eq_residualize_right (Y : V) : residInnerVec H X Y = residInnerVec H X (residualize H Y) := by funext j simpa [residInnerVec] using residualize_inner_swap_right H (X j) Y

Causalean.Mathlib.FWL.residInnerVec_eq_residualize_right · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:237
inner_residualizedRegressor_fwlResidual lemma — The residual left by fwlCoef is orthogonal to every residualized regressor. This is the normal-equation form used in the completing-square argument.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

Y :

V

hQ :

IsUnit (gramResid H X).det

j :

Fin K

conclusion

inner ℝ (residualize H (X j)) (residualize H Y - fittedValue (fun k => residualize H (X k)) (fwlCoef H X Y))
= 0

Proof (Lean source)

lemma inner_residualizedRegressor_fwlResidual (Y : V) (hQ : IsUnit (gramResid H X).det) (j : Fin K) : inner ℝ (residualize H (X j)) (residualize H Y - fittedValue (fun k => residualize H (X k)) (fwlCoef H X Y)) = 0 := by have hne := congrFun (gramResid_mulVec_fwlCoef H X Y hQ) j rw [← sub_eq_zero] rw [inner_sub_right] rw [fittedValue] simp_rw [inner_sum, inner_smul_right] rw [← residualize_inner_swap_right H (X j) Y] have hsum : (∑ x, fwlCoef H X Y x * inner ℝ (residualize H (X j)) (residualize H (X x))) = ∑ x, inner ℝ (residualize H (X j)) (residualize H (X x)) * fwlCoef H X Y x := by apply Finset.sum_congr rfl intro x _hx ring rw [hsum] simpa [mulVec, dotProduct, gramResid, residInnerVec] using sub_eq_zero.mpr hne.symm

Causalean.Mathlib.FWL.inner_residualizedRegressor_fwlResidual · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:262
residualizedObjective_eq_fwlCoef_add_error theorem — Completing-square identity for the residualized objective around the FWL coefficient.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

Y :

V

hQ :

IsUnit (gramResid H X).det

β :

Fin K → ℝ

conclusion

residualizedObjective H X Y β
= residualizedObjective H X Y (fwlCoef H X Y)
+ inner ℝ (fittedValue (fun j => residualize H (X j)) (fun j => fwlCoef H X Y j - β j)) (fittedValue (fun j => residualize H (X j)) (fun j => fwlCoef H X Y j - β j))

Proof (Lean source)

theorem residualizedObjective_eq_fwlCoef_add_error (Y : V) (hQ : IsUnit (gramResid H X).det) (β : Fin K → ℝ) : residualizedObjective H X Y β = residualizedObjective H X Y (fwlCoef H X Y) + inner ℝ (fittedValue (fun j => residualize H (X j)) (fun j => fwlCoef H X Y j - β j)) (fittedValue (fun j => residualize H (X j)) (fun j => fwlCoef H X Y j - β j)) := by let Xtilde : Fin K → V := fun j => residualize H (X j) let b : Fin K → ℝ := fwlCoef H X Y let e : V := residualize H Y - fittedValue Xtilde b let z : V := fittedValue Xtilde (fun j => b j - β j) have hz_eq : z = fittedValue Xtilde b - fittedValue Xtilde β := by dsimp [z, b] rw [fittedValue_sub] have hdecomp : residualize H Y - fittedValue Xtilde β = e + z := by dsimp [e] rw [hz_eq] abel have hcross' : inner ℝ z e = 0 := by dsimp [z, e, Xtilde, b] rw [fittedValue] simp_rw [sum_inner, inner_smul_left] apply Finset.sum_eq_zero intro j _hj have hjzero : inner ℝ (X j - H.starProjection (X j)) (Y - H.starProjection Y - fittedValue (fun j => X j - H.starProjection (X j)) (fwlCoef H X Y)) = 0 := by simpa [residualize] using inner_residualizedRegressor_fwlResidual H X Y hQ j rw [hjzero] simp have hcross : inner ℝ e z = 0 := by rw [real_inner_comm, hcross'] have hpyth : residualizedObjective H X Y β = residualizedObjective H X Y b + inner ℝ z z := by change inner ℝ (residualize H Y - fittedValue Xtilde β) (residualize H Y - fittedValue Xtilde β) = inner ℝ e e + inner ℝ z z rw [hdecomp] rw [inner_add_left, inner_add_right, inner_add_right, hcross, hcross'] ring simpa [z, Xtilde, b] using hpyth

Causalean.Mathlib.FWL.residualizedObjective_eq_fwlCoef_add_error · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:288
fwlCoef_residualized_minimizes theorem — The FWL coefficient minimizes the residualized least-squares objective.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

Y :

V

hQ :

IsUnit (gramResid H X).det

β :

Fin K → ℝ

conclusion

residualizedObjective H X Y (fwlCoef H X Y) ≤ residualizedObjective H X Y β

Proof (Lean source)

theorem fwlCoef_residualized_minimizes (Y : V) (hQ : IsUnit (gramResid H X).det) (β : Fin K → ℝ) : residualizedObjective H X Y (fwlCoef H X Y) ≤ residualizedObjective H X Y β := by rw [residualizedObjective_eq_fwlCoef_add_error H X Y hQ β] exact le_add_of_nonneg_right (by simp)

Causalean.Mathlib.FWL.fwlCoef_residualized_minimizes · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:337
originalObjective_eq_residualizedObjective_add_projectionError theorem — Pythagorean split of the original objective into the residualized objective plus the squared distance from h to the projection of the raw regression residual onto H.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

Y :

V

β :

Fin K → ℝ

h :

V

hh :

h ∈ H

conclusion

originalObjective X Y β h
= residualizedObjective H X Y β
+ inner ℝ (H.orthogonalProjectionFn (Y - fittedValue X β) - h) (H.orthogonalProjectionFn (Y - fittedValue X β) - h)

Proof (Lean source)

theorem originalObjective_eq_residualizedObjective_add_projectionError (Y : V) (β : Fin K → ℝ) {h : V} (hh : h ∈ H) : originalObjective X Y β h = residualizedObjective H X Y β + inner ℝ (H.orthogonalProjectionFn (Y - fittedValue X β) - h) (H.orthogonalProjectionFn (Y - fittedValue X β) - h) := by let v : V := Y - fittedValue X β let r : V := residualize H v let p : V := H.orthogonalProjectionFn v - h have hp_mem : p ∈ H := by exact Submodule.sub_mem H (Submodule.starProjection_apply_mem H v) hh have horth : inner ℝ r p = 0 := by exact inner_residualize_of_mem H v hp_mem have horth' : inner ℝ p r = 0 := by rw [real_inner_comm, horth] have hvh : v - h = r + p := by dsimp [r, p, v] simp have hres_vec : residualize H Y - fittedValue (fun j => residualize H (X j)) β = r := by dsimp [r, v] exact (residualize_regressionResidual H X Y β).symm have hres : residualizedObjective H X Y β = inner ℝ r r := by change inner ℝ (residualize H Y - fittedValue (fun j => residualize H (X j)) β) (residualize H Y - fittedValue (fun j => residualize H (X j)) β) = inner ℝ r r rw [hres_vec] dsimp [originalObjective] change inner ℝ (v - h) (v - h) = residualizedObjective H X Y β + inner ℝ p p rw [hvh, hres] rw [inner_add_left, inner_add_right, inner_add_right, horth, horth'] ring

Causalean.Mathlib.FWL.originalObjective_eq_residualizedObjective_add_projectionError · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:345
residualizedObjective_le_originalObjective theorem — For fixed β, the residualized objective is the minimum of the original objective over the nuisance subspace H.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

Y :

V

β :

Fin K → ℝ

h :

V

hh :

h ∈ H

conclusion

residualizedObjective H X Y β ≤ originalObjective X Y β h

Proof (Lean source)

theorem residualizedObjective_le_originalObjective (Y : V) (β : Fin K → ℝ) {h : V} (hh : h ∈ H) : residualizedObjective H X Y β ≤ originalObjective X Y β h := by rw [originalObjective_eq_residualizedObjective_add_projectionError H X Y β hh] exact le_add_of_nonneg_right (by simp)

Causalean.Mathlib.FWL.residualizedObjective_le_originalObjective · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:383
originalObjective_projection_eq_residualizedObjective theorem — At the nuisance projection, the original objective equals the residualized objective.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

Y :

V

β :

Fin K → ℝ

conclusion

originalObjective X Y β (H.orthogonalProjectionFn (Y - fittedValue X β))
= residualizedObjective H X Y β

Proof (Lean source)

theorem originalObjective_projection_eq_residualizedObjective (Y : V) (β : Fin K → ℝ) : originalObjective X Y β (H.orthogonalProjectionFn (Y - fittedValue X β)) = residualizedObjective H X Y β := by have hmem : H.orthogonalProjectionFn (Y - fittedValue X β) ∈ H := Submodule.starProjection_apply_mem H (Y - fittedValue X β) rw [originalObjective_eq_residualizedObjective_add_projectionError H X Y β hmem] simp

Causalean.Mathlib.FWL.originalObjective_projection_eq_residualizedObjective · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:392
fwlCoef_eq_of_original_minimizer theorem — Any minimizer of the original least-squares problem has coefficient block equal to the FWL coefficient. This is the uniqueness part of the standard FWL statement for the X-block.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

Y :

V

hQ :

IsUnit (gramResid H X).det

β :

Fin K → ℝ

h :

V

hh :

h ∈ H

hmin :

∀ (γ : Fin K → ℝ) {g : V}
if
g ∈ H
then
originalObjective X Y β h ≤ originalObjective X Y γ g

conclusion

β = fwlCoef H X Y

Proof (Lean source)

theorem fwlCoef_eq_of_original_minimizer (Y : V) (hQ : IsUnit (gramResid H X).det) (β : Fin K → ℝ) {h : V} (hh : h ∈ H) (hmin : ∀ (γ : Fin K → ℝ) {g : V}, g ∈ H → originalObjective X Y β h ≤ originalObjective X Y γ g) : β = fwlCoef H X Y := by let Xtilde : Fin K → V := fun j => residualize H (X j) let b : Fin K → ℝ := fwlCoef H X Y let z : V := fittedValue Xtilde (fun j => b j - β j) let hp : V := H.orthogonalProjectionFn (Y - fittedValue X b) have hp_mem : hp ∈ H := by dsimp [hp] exact Submodule.starProjection_apply_mem H (Y - fittedValue X b) have hle₁ : residualizedObjective H X Y β ≤ residualizedObjective H X Y b := by calc residualizedObjective H X Y β ≤ originalObjective X Y β h := residualizedObjective_le_originalObjective H X Y β hh _ ≤ originalObjective X Y b hp := hmin b hp_mem _ = residualizedObjective H X Y b := by simpa [hp] using originalObjective_projection_eq_residualizedObjective H X Y b have hle₂ : residualizedObjective H X Y b ≤ residualizedObjective H X Y β := fwlCoef_residualized_minimizes H X Y hQ β have hres_eq : residualizedObjective H X Y β = residualizedObjective H X Y b := le_antisymm hle₁ hle₂ have hpyth := residualizedObjective_eq_fwlCoef_add_error H X Y hQ β have hz_inner : inner ℝ z z = 0 := by rw [hres_eq] at hpyth have hpyth_z : residualizedObjective H X Y b = residualizedObjective H X Y b + inner ℝ z z := by simpa [z, Xtilde, b] using hpyth linarith have hz0 : z = 0 := inner_self_eq_zero.mp hz_inner let δ : Fin K → ℝ := fun j => b j - β j have hmul : (gramResid H X).mulVec δ = 0 := by funext j have hinner : inner ℝ (residualize H (X j)) z = 0 := by rw [hz0, inner_zero_right] dsimp [z, Xtilde, δ] at hinner ⊢ rw [fittedValue] at hinner simp_rw [inner_sum, inner_smul_right] at hinner simpa [mulVec, dotProduct, gramResid, mul_comm] using hinner have hδ0 : δ = 0 := Matrix.eq_zero_of_mulVec_eq_zero hQ.ne_zero hmul funext j have hj := congrFun hδ0 j dsimp [δ, b] at hj linarith

Causalean.Mathlib.FWL.fwlCoef_eq_of_original_minimizer · Causalean/Mathlib/Analysis/InnerProductSpace/FrischWaughLovell.lean:426

Gram 3 core · 0 supporting The file defines the Gram matrix gram k x, the positive-semidefinite-kernel predicate IsPSDkernel, and the regularized-Gram positive-definiteness theorem gram_add_lambda_posDef: if k is positive semidefinite and λ > 0, t ★ IsPSDkernel★ gram_add_lambda_posDef

Gram matrices of a kernel

The file defines the Gram matrix gram k x, the positive-semidefinite-kernel predicate IsPSDkernel, and the regularized-Gram positive-definiteness theorem gram_add_lambda_posDef: if k is positive semidefinite and λ > 0, then K + λI ≻ 0. This is the finite-sample invertibility fact used by kernel ridge regression.

def gram reviewed

Causalean.Mathlib.Analysis.InnerProductSpace

For an input space, a sample size, a real-valued kernel on that space, and a sample of that size, the Gram matrix is the matrix whose row- $i$ , column- $j$ entry is the kernel evaluated at the $i$ th and $j$ th sample points.

Definition (Lean source)

parameters

X :

Type*

n :

ℕ

k :

X → X → ℝ

x :

Fin n → X

def

gram k x :

Matrix (Fin n) (Fin n) ℝ

given by

fun i j => k (x i) (x j)

Causalean.Mathlib.Analysis.InnerProductSpace.gram · Causalean/Mathlib/Analysis/InnerProductSpace/Gram.lean:26

def IsPSDkernel reviewed

Causalean.Mathlib.Analysis.InnerProductSpace

For an input space and a real-valued kernel on that space, the positive-semidefinite-kernel property holds exactly when, for every finite sample, its Gram matrix is positive semidefinite.

Definition (Lean source)

parameters

X :

Type*

k :

X → X → ℝ

n :

ℕ

x :

Fin n → X

def

IsPSDkernel k :

Prop

given by

(gram k x).PosSemidef

Causalean.Mathlib.Analysis.InnerProductSpace.IsPSDkernel · Causalean/Mathlib/Analysis/InnerProductSpace/Gram.lean:33

theorem gram_add_lambda_posDef reviewed

Causalean.Mathlib.Analysis.InnerProductSpace

For a finite sample x and kernel k, if k is positive semidefinite, i.e. every Gram matrix it produces is PSD and the regularization level lam is strictly positive, then the regularized Gram matrix gram k x + lam·I is positive definite, hence invertible.

Formal statement

hypotheses

X :

Type*

n :

ℕ

k :

X → X → ℝ

hk :

IsPSDkernel k

x :

Fin n → X

lam :

ℝ

hlam :

0 < lam

conclusion

(gram k x + lam • (1 : Matrix (Fin n) (Fin n) ℝ)).PosDef

Proof (Lean source)

theorem gram_add_lambda_posDef {X : Type*} {n : ℕ} {k : X → X → ℝ} (hk : IsPSDkernel k) (x : Fin n → X) {lam : ℝ} (hlam : 0 < lam) : (gram k x + lam • (1 : Matrix (Fin n) (Fin n) ℝ)).PosDef := by have hpsd : (gram k x).PosSemidef := hk n x have hI : (lam • (1 : Matrix (Fin n) (Fin n) ℝ)).PosDef := by exact Matrix.PosDef.smul Matrix.PosDef.one hlam exact Matrix.PosDef.posSemidef_add hpsd hI

Causalean.Mathlib.Analysis.InnerProductSpace.gram_add_lambda_posDef · Causalean/Mathlib/Analysis/InnerProductSpace/Gram.lean:39 · uses IsPSDkernel , gram

Projection 1 core · 0 supporting This file proves exists_orthogonalProjection_of_posSemidef: every finite-dimensional subspace of a vector space over a linearly ordered field admits a linear map into that subspace whose residual is orthogonal, with resp ★ exists_orthogonalProjection_of_posSemidef

Semidefinite Normal-Equation Maps

This file proves exists_orthogonalProjection_of_posSemidef: every finite-dimensional subspace of a vector space over a linearly ordered field admits a linear map into that subspace whose residual is orthogonal, with respect to a symmetric positive-semidefinite bilinear form, to every vector in the subspace. The result supplies the linear-algebra substrate for weighted normal-equation arguments where the inner product may be degenerate.

lemma exists_orthogonalProjection_of_posSemidef reviewed

Causalean.Mathlib

In a vector space over a linearly ordered field equipped with a bilinear form B that is symmetric and positive-semidefinite, every finite-dimensional linear subspace H admits a linear self-map P of the ambient space, valued in H, whose residual X - P X is B-orthogonal to every vector of H, for every X.

Formal statement

hypotheses

K :

Type u_1

shared

V :

Type u_2

shared

B :

BilinForm K V

hsymm :

∀ x y, B x y = B y x

hpos :

∀ x, 0 ≤ B x x

H :

Submodule K V

FiniteDimensional K H

conclusion

∃ P : V →ₗ[K] V,

conclusion 1

X :

P X ∈ H

conclusion 2

X :

h ∈ H :

B (X - P X) h = 0

Proof (Lean source)

lemma exists_orthogonalProjection_of_posSemidef (B : BilinForm K V) (hsymm : ∀ x y, B x y = B y x) (hpos : ∀ x, 0 ≤ B x x) (H : Submodule K V) [FiniteDimensional K H] : ∃ P : V →ₗ[K] V, (∀ X, P X ∈ H) ∧ (∀ X, ∀ h ∈ H, B (X - P X) h = 0) := by classical let A : H →ₗ[K] Module.Dual K H := LinearMap.mk₂ K (fun x y : H => B x.1 y.1) (by intro x y z simp) (by intro a x z simp) (by intro x y z simp) (by intro a x z simp) let L : V →ₗ[K] Module.Dual K H := LinearMap.mk₂ K (fun (x : V) (y : H) => B x y.1) (by intro x y z simp) (by intro a x z simp) (by intro x y z simp) (by intro a x z simp) have hBsymm : B.IsSymm := ⟨fun x y => hsymm x y⟩ have hAflip : A.flip = A := by ext x y simpa [A] using (hsymm x.1 y.1).symm have hL_mem_range : ∀ X, L X ∈ range A := by intro X have hL_ann : L X ∈ (ker A).dualAnnihilator := by rw [Submodule.mem_dualAnnihilator] intro x hx have hxself : B x.1 x.1 = 0 := by have hAx : A x = 0 := by simpa [LinearMap.mem_ker] using hx have := congrArg (fun f : Module.Dual K H => f x) hAx simpa [A] using this have hxker : x.1 ∈ ker B := by exact (B.apply_apply_same_eq_zero_iff hpos hBsymm).mp hxself have hxX : B x.1 X = 0 := by have hBx : B x.1 = 0 := by simpa [LinearMap.mem_ker] using hxker have := congrArg (fun f : Module.Dual K V => f X) hBx simpa using this simpa [L, hsymm X x.1] using hxX rwa [LinearMap.dualAnnihilator_ker_eq_range_flip, hAflip] at hL_ann let Lrange : V →ₗ[K] range A := L.codRestrict (range A) hL_mem_range letI : Module.Free K (range A) := Module.Free.of_divisionRing K (range A) obtain ⟨S, hS⟩ := A.rangeRestrict.exists_rightInverse_of_surjective (LinearMap.range_rangeRestrict A) let PH : V →ₗ[K] H := S.comp Lrange refine ⟨H.subtype.comp PH, ?_, ?_⟩ · intro X exact (PH X).2 · intro X h hH let hh : H := ⟨h, hH⟩ have hEq : A (PH X) hh = L X hh := by have hRangeEq : A.rangeRestrict (S (Lrange X)) = Lrange X := by exact congrArg (fun f : range A →ₗ[K] range A => f (Lrange X)) hS have hValEq : (A.rangeRestrict (S (Lrange X)) : Module.Dual K H) = (Lrange X : Module.Dual K H) := congrArg (fun y : range A => (y : Module.Dual K H)) hRangeEq exact congrArg (fun f : Module.Dual K H => f hh) hValEq have hB_eq : B (PH X).1 h = B X h := by simpa [A, L, PH, hh] using hEq simp [hB_eq]

Causalean.Mathlib.exists_orthogonalProjection_of_posSemidef · Causalean/Mathlib/Analysis/InnerProductSpace/Projection.lean:45

RKHS 1 core · 0 supporting Mathlib's RKHS class describes Hilbert spaces continuously embedded in a function space and constructs kernel functions under completeness assumptions. ★ HasReproducingRepresenters

Abstract reproducing representers

Mathlib's RKHS class describes Hilbert spaces continuously embedded in a function space and constructs kernel functions under completeness assumptions. The HasReproducingRepresenters proposition here records only the identity f x = ⟪f, kₓ⟫ for a supplied evaluation and representer map. It does not assert that evaluation embeds H into a function space. This is the interface consumed by the representer theorem and the representer-ball Rademacher bound.

structure HasReproducingRepresenters reviewed

Causalean.ML

A real inner-product space has reproducing representers for a domain, an evaluation map, and a representer map when evaluation equals inner product against the point's representer. This does not assert that evaluation embeds the space into a function space.

Definition (Lean source)

parameters

X H :

Type*

NormedAddCommGroup H

InnerProductSpace ℝ H

feval :

H → X → ℝ

representer :

X → H

assumes

reproducing :

∀ (f : H) (x : X), feval f x = inner ℝ f (representer x)

The reproducing identity f x = ⟪f, kₓ⟫.

Causalean.ML.HasReproducingRepresenters · Causalean/Mathlib/Analysis/InnerProductSpace/RKHS.lean:24

Mathlib.Analysis.Inner­Product­Space

Frisch-Waugh-Lovell Algebra

Gram matrices of a kernel

Semidefinite Normal-Equation Maps

Abstract reproducing representers

Mathlib.Analysis.InnerProductSpace