Panel.Analysis
Population residualization for Frisch-Waugh-Lovell estimand characterization: linear nuisance classes in L²(μ), residualization witnesses, and the residualized regression coefficient characterized from the normal equations.
Residualization 4 core · 0 supporting This file defines the population residualization primitives used by Frisch-Waugh-Lovell style estimand-characterization results. ★ residualizedCoefficient_eq_of_normalEqs
Population Residualization
This file defines the population residualization primitives used by Frisch-Waugh-Lovell style estimand-characterization results. It is independent of any particular potential-outcome system so paper-specific modules can instantiate the same nuisance-class interface.
structure LinearL2Class reviewed
⚑ flagged
Causalean.Panel
A linear square-integrable class is a nuisance space of real-valued functions, cut out by a membership predicate mem, that is closed under the zero function, closed under addition, and closed under real scalar multiplication, with every member square-integrable.
Definition (Lean source)
parameters
Ω :
Type*
μ :
Measure Ω
fields
The membership predicate cutting out `H ⊆ (Ω → ℝ)`.
mem :
(Ω → ℝ) → Prop
Every member is square-integrable.
memLp :
∀ ⦃f : Ω → ℝ⦄
if
mem f
then
MemLp f 2 μ
The class contains the zero function.
zero_mem :
mem (fun _ => (0 : ℝ))
The class is closed under addition.
add_mem :
∀ ⦃f g : Ω → ℝ⦄
if
mem f
and
mem g
then
mem (f + g)
The class is closed under scalar multiplication.
smul_mem :
∀ (c : ℝ) ⦃f : Ω → ℝ⦄
if
mem f
then
mem (c • f)
structure ResidualizationWitness reviewed
⚑ flagged
Causalean.Panel
A residualization witness decomposes a real-valued function V into an in-class projection VH and a square-integrable residual Vtilde such that V equals their sum almost everywhere and the residual is orthogonal in expectation to every member of the nuisance class.
Definition (Lean source)
parameters
fields
The in-class projection `V_H ∈ H`.
VH :
Ω → ℝ
The residual `Ṽ`.
Vtilde :
Ω → ℝ
The projection lies in the nuisance class.
VH_mem :
H.mem VH
The residual is square-integrable.
Vtilde_memLp :
MemLp Vtilde 2 μ
Almost-everywhere decomposition `V = VH + Vtilde`.
decomp :
V =ᵐ[μ] VH + Vtilde
Population orthogonality: the residual is uncorrelated with every
member of `H`.
orthogonal :
∀ ⦃h : Ω → ℝ⦄
if
H.mem h
then
∫ ω, Vtilde ω * h ω ∂μ = 0
def residualizedCoefficient reviewed
⚑ flagged
Causalean.Panel
The residualized population coefficient is the ratio of the covariance-like integral of treatment and outcome residuals to the second moment of the treatment residual.
Definition (Lean source)
noncomputable def residualizedCoefficient {Ω : Type*} [MeasurableSpace Ω]
(μ : Measure Ω) (H : LinearL2Class μ) {Y D : Ω → ℝ}
(wY : ResidualizationWitness μ H Y)
(wD : ResidualizationWitness μ H D) : ℝ :=
(∫ ω, wD.Vtilde ω * wY.Vtilde ω ∂μ) / (∫ ω, wD.Vtilde ω * wD.Vtilde ω ∂μ)
theorem residualizedCoefficient_eq_of_normalEqs reviewed
⚑ flagged
Causalean.Panel
Population Frisch-Waugh-Lovell theorem (prop:po-estimand-fwl). Let wY and wD be residualization witnesses decomposing outcome Y and treatment D each into a component of a common linear square-integrable nuisance class H plus an orthogonal residual. If the second moment of the treatment residual is strictly positive, and a nuisance-class element Hβ together with a coefficient β are such that the combined residual Y − β·D − Hβ is square-integrable, orthogonal in expectation to D, and orthogonal in expectation to every member of H, then β equals the ratio of the covariance-like integral of the outcome and treatment residuals Ỹ and D̃ to the second moment of D̃, i.e. the residualized coefficient residualizedCoefficient μ H wY wD.
Formal statement
hypotheses
Ω :
Type*
μ :
Measure Ω
H :
Y D :
Ω → ℝ
wY :
ResidualizationWitness μ H Y
wD :
ResidualizationWitness μ H D
hDtilde_pos :
0 < ∫ ω, wD.Vtilde ω * wD.Vtilde ω ∂μ
β :
ℝ
Hβ :
Ω → ℝ
Hβ_mem :
H.mem Hβ
e_mem :
MemLp (fun ω => Y ω - β * D ω - Hβ ω) 2 μ
h_normal_D :
∫ ω, (Y ω - β * D ω - Hβ ω) * D ω ∂μ = 0
h_normal_H :
∀ ⦃h : Ω → ℝ⦄
if
H.mem h
then
∫ ω, (Y ω - β * D ω - Hβ ω) * h ω ∂μ = 0
conclusion
β = residualizedCoefficient μ H wY wD
Proof (Lean source)
theorem residualizedCoefficient_eq_of_normalEqs {Ω : Type*} [MeasurableSpace Ω]
(μ : Measure Ω) (H : LinearL2Class μ)
{Y D : Ω → ℝ}
(wY : ResidualizationWitness μ H Y)
(wD : ResidualizationWitness μ H D)
(hDtilde_pos : 0 < ∫ ω, wD.Vtilde ω * wD.Vtilde ω ∂μ)
(β : ℝ) (Hβ : Ω → ℝ) (Hβ_mem : H.mem Hβ)
(e_mem : MemLp (fun ω => Y ω - β * D ω - Hβ ω) 2 μ)
(h_normal_D : ∫ ω, (Y ω - β * D ω - Hβ ω) * D ω ∂μ = 0)
(h_normal_H : ∀ ⦃h : Ω → ℝ⦄, H.mem h →
∫ ω, (Y ω - β * D ω - Hβ ω) * h ω ∂μ = 0) :
β = residualizedCoefficient μ H wY wD := by
let e : Ω → ℝ := fun ω => Y ω - β * D ω - Hβ ω
let h_star : Ω → ℝ := fun ω => -Hβ ω + (wY.VH ω + (-β) * wD.VH ω)
have Hβ_mem' : MemLp Hβ 2 μ := H.memLp Hβ_mem
have h_star_mem : H.mem h_star := by
have h_neg_Hβ : H.mem (fun ω => -Hβ ω) := by
have h := H.smul_mem (-1 : ℝ) Hβ_mem
have hfun : ((-1 : ℝ) • Hβ) = fun ω => -Hβ ω := by
funext ω; simp
rwa [hfun] at h
have h_beta : H.mem (fun ω => (-β) * wD.VH ω) := by
have h := H.smul_mem (-β) wD.VH_mem
have hfun : ((-β : ℝ) • wD.VH) = fun ω => (-β) * wD.VH ω := by
funext ω; simp
rwa [hfun] at h
have h_inner : H.mem (fun ω ↦ wY.VH ω + (-β) * wD.VH ω) := H.add_mem wY.VH_mem h_beta
exact H.add_mem h_neg_Hβ h_inner
have h_orth : ∫ ω, wD.Vtilde ω * h_star ω ∂μ = 0 := wD.orthogonal h_star_mem
have e_mem' : MemLp e 2 μ := by simpa [e] using e_mem
have hD_decomp_int : ∫ ω, e ω * D ω ∂μ = ∫ ω, e ω * (wD.VH ω + wD.Vtilde ω) ∂μ := by
refine integral_congr_ae ?_
filter_upwards [wD.decomp] with ω hD
simp [e, hD]
have hD_VH_plus_Vtilde : ∫ ω, e ω * (wD.VH ω + wD.Vtilde ω) ∂μ = 0 := by
calc
∫ ω, e ω * (wD.VH ω + wD.Vtilde ω) ∂μ = ∫ ω, e ω * D ω ∂μ := hD_decomp_int.symm
_ = 0 := by simpa [e] using h_normal_D
have h_mul_split : (fun ω => e ω * (wD.VH ω + wD.Vtilde ω)) =ᵐ[μ]
(fun ω => e ω * wD.VH ω + e ω * wD.Vtilde ω) := by
exact Filter.EventuallyEq.of_eq (by
funext ω
ring)
have h_mul_split_int :
(∫ ω, e ω * wD.VH ω ∂μ) + ∫ ω, e ω * wD.Vtilde ω ∂μ =
∫ ω, e ω * (wD.VH ω + wD.Vtilde ω) ∂μ := by
calc
(∫ ω, e ω * wD.VH ω ∂μ) + ∫ ω, e ω * wD.Vtilde ω ∂μ =
∫ ω, e ω * wD.VH ω + e ω * wD.Vtilde ω ∂μ := by
have hVH_int : Integrable (fun ω => e ω * wD.VH ω) μ :=
e_mem'.integrable_mul (H.memLp wD.VH_mem)
have hVt_int : Integrable (fun ω => e ω * wD.Vtilde ω) μ :=
e_mem'.integrable_mul wD.Vtilde_memLp
exact (integral_add hVH_int hVt_int).symm
_ = ∫ ω, e ω * (wD.VH ω + wD.Vtilde ω) ∂μ :=
(integral_congr_ae h_mul_split).symm
have hVH : ∫ ω, e ω * wD.VH ω ∂μ = 0 := by simpa [e] using h_normal_H wD.VH_mem
have h_eVtilde_int : ∫ ω, e ω * wD.Vtilde ω ∂μ = 0 := by
have hsplit :
(∫ ω, e ω * wD.VH ω ∂μ) + ∫ ω, e ω * wD.Vtilde ω ∂μ = 0 := by
calc
(∫ ω, e ω * wD.VH ω ∂μ) + ∫ ω, e ω * wD.Vtilde ω ∂μ
= ∫ ω, e ω * (wD.VH ω + wD.Vtilde ω) ∂μ := h_mul_split_int
_ = 0 := hD_VH_plus_Vtilde
linarith [hsplit, hVH]
have h_eVtilde_mul : ∫ ω, wD.Vtilde ω * e ω ∂μ = 0 := by
simpa [mul_comm] using h_eVtilde_int
have hV_decomp :
(fun ω => wD.Vtilde ω * e ω) =ᵐ[μ]
(fun ω => wD.Vtilde ω * (h_star ω + (wY.Vtilde ω - β * wD.Vtilde ω))) := by
filter_upwards [wY.decomp, wD.decomp] with ω hY hD
have hE : e ω = h_star ω + (wY.Vtilde ω - β * wD.Vtilde ω) := by
simp [e, h_star, hY, hD]
ring
rw [hE]
have hV_mul_split :
(fun ω => wD.Vtilde ω * (h_star ω + (wY.Vtilde ω - β * wD.Vtilde ω))) =ᵐ[μ]
(fun ω => wD.Vtilde ω * h_star ω + wD.Vtilde ω * (wY.Vtilde ω - β * wD.Vtilde ω)) := by
exact Filter.EventuallyEq.of_eq (by
funext ω
ring)
have h_star_int : Integrable (fun ω => wD.Vtilde ω * h_star ω) μ :=
wD.Vtilde_memLp.integrable_mul (H.memLp h_star_mem)
have h_second_mem : MemLp (fun ω => wY.Vtilde ω - β * wD.Vtilde ω) 2 μ :=
wY.Vtilde_memLp.sub (MemLp.const_mul wD.Vtilde_memLp β)
have h_second_int : Integrable (fun ω => wD.Vtilde ω * (wY.Vtilde ω - β * wD.Vtilde ω)) μ :=
wD.Vtilde_memLp.integrable_mul h_second_mem
have h_expanded :
∫ ω, wD.Vtilde ω * e ω ∂μ =
∫ ω, wD.Vtilde ω * h_star ω ∂μ + ∫ ω, wD.Vtilde ω * (wY.Vtilde ω - β * wD.Vtilde ω) ∂μ := by
calc
∫ ω, wD.Vtilde ω * e ω ∂μ =
∫ ω, wD.Vtilde ω * h_star ω + wD.Vtilde ω * (wY.Vtilde ω - β * wD.Vtilde ω) ∂μ := by
exact integral_congr_ae (hV_decomp.trans hV_mul_split)
_ = ∫ ω, wD.Vtilde ω * h_star ω ∂μ + ∫ ω, wD.Vtilde ω * (wY.Vtilde ω - β * wD.Vtilde ω) ∂μ :=
integral_add h_star_int h_second_int
have h_num_zero : ∫ ω, wD.Vtilde ω * (wY.Vtilde ω - β * wD.Vtilde ω) ∂μ = 0 := by
linarith [h_expanded, h_eVtilde_mul, h_orth]
have hβ_mul : ∫ ω, wD.Vtilde ω * (β * wD.Vtilde ω) ∂μ =
β * ∫ ω, wD.Vtilde ω * wD.Vtilde ω ∂μ := by
have htmp :
(fun ω => wD.Vtilde ω * (β * wD.Vtilde ω)) =ᵐ[μ]
(fun ω => β * (wD.Vtilde ω * wD.Vtilde ω)) := by
exact Filter.EventuallyEq.of_eq (by
funext ω
ring)
calc
∫ ω, wD.Vtilde ω * (β * wD.Vtilde ω) ∂μ = ∫ ω, β * (wD.Vtilde ω * wD.Vtilde ω) ∂μ :=
integral_congr_ae htmp
_ = β * ∫ ω, wD.Vtilde ω * wD.Vtilde ω ∂μ := by
simp [integral_const_mul]
have h_num_expand :
∫ ω, wD.Vtilde ω * (wY.Vtilde ω - β * wD.Vtilde ω) ∂μ
= ∫ ω, wD.Vtilde ω * wY.Vtilde ω ∂μ
- β * ∫ ω, wD.Vtilde ω * wD.Vtilde ω ∂μ := by
have htmp :
(fun ω => wD.Vtilde ω * (wY.Vtilde ω - β * wD.Vtilde ω)) =ᵐ[μ]
(fun ω => wD.Vtilde ω * wY.Vtilde ω - wD.Vtilde ω * (β * wD.Vtilde ω)) := by
exact Filter.EventuallyEq.of_eq (by
funext ω
ring)
have h1 : Integrable (fun ω => wD.Vtilde ω * wY.Vtilde ω) μ :=
wD.Vtilde_memLp.integrable_mul wY.Vtilde_memLp
have h2 : Integrable (fun ω => wD.Vtilde ω * (β * wD.Vtilde ω)) μ :=
wD.Vtilde_memLp.integrable_mul (MemLp.const_mul wD.Vtilde_memLp β)
calc
∫ ω, wD.Vtilde ω * (wY.Vtilde ω - β * wD.Vtilde ω) ∂μ =
∫ ω, wD.Vtilde ω * wY.Vtilde ω - wD.Vtilde ω * (β * wD.Vtilde ω) ∂μ :=
integral_congr_ae htmp
_ = ∫ ω, wD.Vtilde ω * wY.Vtilde ω ∂μ - ∫ ω, wD.Vtilde ω * (β * wD.Vtilde ω) ∂μ :=
integral_sub h1 h2
_ = ∫ ω, wD.Vtilde ω * wY.Vtilde ω ∂μ - β * ∫ ω, wD.Vtilde ω * wD.Vtilde ω ∂μ := by
rw [hβ_mul]
have hcoeff : β * ∫ ω, wD.Vtilde ω * wD.Vtilde ω ∂μ = ∫ ω, wD.Vtilde ω * wY.Vtilde ω ∂μ := by
have hzero := h_num_zero
rw [h_num_expand] at hzero
linarith
have hdenom_ne : (∫ ω, wD.Vtilde ω * wD.Vtilde ω ∂μ) ≠ 0 := hDtilde_pos.ne'
have hβ_eq : β = (∫ ω, wD.Vtilde ω * wY.Vtilde ω ∂μ) / (∫ ω, wD.Vtilde ω * wD.Vtilde ω ∂μ) :=
(eq_div_iff hdenom_ne).2 hcoeff
simpa [residualizedCoefficient] using hβ_eq