Stat.Linear­Model

LinearModel — FWLInstanceL2.

Gauss­Markov 12 core · 8 supporting · 5 submodules Algebraic and probabilistic ingredients used in finite Gauss–Markov arguments. OLSAsymptotics 54 core · 38 supporting · 7 submodules Heteroskedastic OLS asymptotics: population and sample moment objects, sandwich covariance estimators, and score regularity conditions.
FWLInstance­L2 1 core · 4 supporting This file instantiates the abstract Frisch-Waugh-Lovell development on square-integrable real functions under a probability measure. ★ fwlCoef_eq_of_original_minimizer

L2 Frisch-Waugh-Lovell Instance

This file instantiates the abstract Frisch-Waugh-Lovell development on square-integrable real functions under a probability measure. It supplies orthogonal projections for finite-dimensional nuisance subspaces, identifies the Lp inner product with the corresponding population integral, and exposes the residualized normal equations, least-squares optimality, and uniqueness statements for the L²(μ) specialization.

theorem fwlCoef_eq_of_original_minimizer reviewed
Causalean.Stat.FWLInstanceL2

FWL uniqueness on L²(μ). Fix square-integrable regressors X and outcome Y, and a finite-dimensional nuisance subspace H of L²(μ), and assume the residualized regressor Gram matrix is invertible. If the nuisance term h lies in H and the pair (β, h) minimizes the original least-squares objective jointly over all coefficient vectors and nuisance terms in H, then β equals the Frisch–Waugh–Lovell coefficient computed by residualizing against H. Specialization of Causalean.Mathlib.FWL.fwlCoef_eq_of_original_minimizer.

Formal statement
hypotheses
α :
Type u_1
Measure α
shared
K :
ℕ
shared
H :
Submodule ℝ ↥(Lp ℝ 2 μ)
shared
X :
Fin K → ↥(Lp ℝ 2 μ)
shared
Y :
↥(Lp ℝ 2 μ)
shared
hQ :
IsUnit (gramResid H X).det
β :
Fin K → ℝ
h :
Lp ℝ 2 μ
hh :
h ∈ H
hmin :
∀ (γ : Fin K → ℝ) {g : Lp ℝ 2 μ}
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 (hQ : IsUnit (gramResid H X).det) (β : Fin K → ℝ) {h : Lp ℝ 2 μ} (hh : h ∈ H) (hmin : ∀ (γ : Fin K → ℝ) {g : Lp ℝ 2 μ}, g ∈ H → originalObjective X Y β h ≤ originalObjective X Y γ g) : β = fwlCoef H X Y := fwlCoef_eq_of_original_minimizer H X Y hQ β hh hmin
Causalean.Stat.FWLInstanceL2.fwlCoef_eq_of_original_minimizer · Causalean/Stat/LinearModel/FWLInstanceL2.lean:83 · uses fwlCoef , gramResid , originalObjective
4 supporting declarations (lemmas, instances)
  • hasOrthogonalProjection_of_finiteDimensional instance — For a measurable sample space, a measure on that sample space, and a finite-dimensional real linear subspace of the square-integrable real functions under that measure, an orthogonal projection onto that subspace exists.
    parameters
    α :
    Type u_1
    Measure α
    shared
    H :
    Submodule ℝ (Lp ℝ 2 μ)
    FiniteDimensional ℝ H
    instance
    hasOrthogonalProjection_of_finiteDimensional H :
    H.HasOrthogonalProjection
    given by
    inferInstance
    Causalean.Stat.FWLInstanceL2.hasOrthogonalProjection_of_finiteDimensional · Causalean/Stat/LinearModel/FWLInstanceL2.lean:32
  • inner_eq_integral theorem — L² inner product = integral pairing. For two square-integrable real random variables, the Hilbert-space inner product equals the integral of their product, independent of the chosen representatives. This is the bridge between abstract FWL inner products and the population second moments used in estimand papers.
    hypotheses
    α :
    Type u_1
    Measure α
    shared
    f g :
    Lp ℝ 2 μ
    conclusion
    inner ℝ f g = ∫ a, f a * g a ∂μ
    Proof (Lean source)
    theorem inner_eq_integral (f g : Lp ℝ 2 μ) : inner ℝ f g = ∫ a, f a * g a ∂μ := by rw [L2.inner_def] refine integral_congr_ae (Filter.Eventually.of_forall (fun a => ?_)) change inner ℝ (f a) (g a) = f a * g a exact mul_comm _ _
    Causalean.Stat.FWLInstanceL2.inner_eq_integral · Causalean/Stat/LinearModel/FWLInstanceL2.lean:43
  • gramResid_mulVec_fwlCoef theorem — Residualized normal equations on L²(μ). The FWL coefficient solves gramResid H X *ᵥ fwlCoef H X Y = residInnerVec H X Y whenever the residualized Gram matrix is invertible. Specialization of Causalean.Mathlib.FWL.gramResid_mulVec_fwlCoef.
    hypotheses
    α :
    Type u_1
    Measure α
    shared
    K :
    ℕ
    shared
    H :
    Submodule ℝ ↥(Lp ℝ 2 μ)
    shared
    X :
    Fin K → ↥(Lp ℝ 2 μ)
    shared
    Y :
    ↥(Lp ℝ 2 μ)
    shared
    hQ :
    IsUnit (gramResid H X).det
    conclusion
    (gramResid H X).mulVec (fwlCoef H X Y)
    = residInnerVec H X Y
    Proof (Lean source)
    theorem gramResid_mulVec_fwlCoef (hQ : IsUnit (gramResid H X).det) : (gramResid H X).mulVec (fwlCoef H X Y) = residInnerVec H X Y := gramResid_mulVec_fwlCoef H X Y hQ
    Causalean.Stat.FWLInstanceL2.gramResid_mulVec_fwlCoef · Causalean/Stat/LinearModel/FWLInstanceL2.lean:60
  • fwlCoef_original_minimizes theorem — FWL least-squares optimality on L²(μ). The FWL coefficient (paired with the nuisance projection of its raw residual) minimizes the original least-squares objective over coefficients and nuisance terms in H. Specialization of Causalean.Mathlib.FWL.fwlCoef_original_minimizes.
    hypotheses
    α :
    Type u_1
    Measure α
    shared
    K :
    ℕ
    shared
    H :
    Submodule ℝ ↥(Lp ℝ 2 μ)
    shared
    X :
    Fin K → ↥(Lp ℝ 2 μ)
    shared
    Y :
    ↥(Lp ℝ 2 μ)
    shared
    hQ :
    IsUnit (gramResid H X).det
    β :
    Fin K → ℝ
    h :
    Lp ℝ 2 μ
    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 (hQ : IsUnit (gramResid H X).det) (β : Fin K → ℝ) {h : Lp ℝ 2 μ} (hh : h ∈ H) : originalObjective X Y (fwlCoef H X Y) (H.orthogonalProjectionFn (Y - fittedValue X (fwlCoef H X Y))) ≤ originalObjective X Y β h := fwlCoef_original_minimizes H X Y hQ β hh
    Causalean.Stat.FWLInstanceL2.fwlCoef_original_minimizes · Causalean/Stat/LinearModel/FWLInstanceL2.lean:70