Panel.EstimandCharacterization.FlexibleDIDMundlak
Wooldridge's extended TWFE: the equivalence of pooled OLS with saturated interactions and imputation-style estimands.
DID 26 core · 6 supporting This file provides finite-cell primitives for Wooldridge-style flexible imputation, pooled least squares, and extended two-way fixed effects difference-in-differences estimands. ★ recovers_target_Y0★ thetaPOLS_eq_imputationTheta★ thetaETWFE_eq_imputationTheta★ flexible_did_cell_characterization★ flexible_did_aggregate_characterization★ flexible_did_scaffold_characterization
Wooldridge Flexible DID Cells
This file provides finite-cell primitives for Wooldridge-style flexible
imputation, pooled least squares, and extended two-way fixed effects
difference-in-differences estimands. It defines staggered-adoption cell means,
support conditions, untreated-outcome regressions, normal-equation-based
POLS/ETWFE coefficients, and aggregate ATT quantities. The main public theorem
is flexible_did_scaffold_characterization, the finite-cell characterization, with cell and
aggregate components
available as flexible_did_cell_characterization and
flexible_did_aggregate_characterization.
Finite staggered-adoption cell system: cohort shares and within-cohort covariate weights over treated and untreated cohort-time cells, with cell-level means of the untreated and cohort-specific treated potential outcomes. It requires that every treated cell's cohort has positive share, that the covariate weights are nonnegative and sum to one within each cohort, and that the observed cell mean coincides with the treated mean on treated cells and with the untreated mean on untreated cells.
Definition (Lean source)
For finite sets of cohorts, periods, and covariate cells and a staggered-adoption cell system, the treated-cell set is the finite set of all cohort--period pairs designated as treated by that system.
Definition (Lean source)
For finite sets of cohorts, periods, and covariate cells and a staggered-adoption cell system, the untreated-cell set is the finite set of all cohort--period pairs designated as untreated and used to fit the untreated-outcome regression.
Definition (Lean source)
For finite sets of cohorts, periods, and covariate cells, a staggered-adoption cell system, a cohort, and a period, the cell average treatment effect on the treated is the covariate- weighted average, within that cohort, of the treated potential outcome minus the untreated potential outcome in that period.
Definition (Lean source)
For finite sets of cohorts, periods, and covariate cells, a staggered-adoption cell system, and a cohort-period weighting function, the aggregate average treatment effect on the treated is the weighted sum of cell average treatment effects over all treated cells.
Definition (Lean source)
Nonnegative aggregate weights summing to one on the target treated cells.
Definition (Lean source)
For finite sets of cohorts, periods, and covariate cells and a staggered-adoption cell system, no anticipation means that, for every cohort, every period designated untreated, and every covariate cell, that cohort's potential outcome equals its untreated potential outcome.
Definition (Lean source)
For finite sets of cohorts, periods, and covariate cells and a staggered-adoption cell system, conditional parallel trends in additive form means that there exist cohort-by-covariate and period-by- covariate functions whose sum equals the untreated potential-outcome mean for every cohort, period, and covariate cell.
Definition (Lean source)
For finite sets of cohorts, periods, and covariate cells and a cohort-period-covariate function, the cell-additivity condition means that there exist cohort-by-covariate and period-by- covariate functions whose sum equals that function at every cell.
Definition (Lean source)
For finite sets of cohorts, periods, and covariate cells and a staggered-adoption cell system, the untreated-design identification condition means that every additive cohort-period- covariate function which vanishes at every untreated cell also vanishes at every treated cell.
Definition (Lean source)
A finite-cell weighted least-squares fit of the untreated-outcome mean for a staggered cell design P, restricted to the untreated observations. It bundles a fitted untreated-outcome mean that is additive in cohort and time given the covariate cell, projection weights that are strictly positive on the untreated design, the requirement that the fit solves the covariate/cell-weighted normal equations against every additive test function, summed over the untreated design, full-rank identification of the additive class from vanishing on the untreated design alone, and a positive cohort share on every treated cell.
Definition (Lean source)
The part of an untreated-regression witness needed to prove exact fit on the untreated design.
Definition (Lean source)
For finite sets of cohorts, periods, and covariate cells, the staggered-adoption cell system underlying the regression, and a saturated untreated-outcome regression, the untreated-fit witness retains its fitted untreated mean, additivity, untreated-cell weights, positivity condition, and untreated normal equations, while omitting its target-support and design-identification conditions.
Definition (Lean source)
Saturated untreated regression recovers the untreated potential outcome on treated cells. If no anticipation holds: the treated and untreated potential-outcome means agree on every cell in the untreated-outcome regression's design and conditional parallel trends holds — the mean untreated potential outcome admits an additive cohort/time fixed-effects representation given covariates, then on any treated cohort-time cell (g,t) covered by the saturated untreated regression S, the fitted value S.m0 g t c equals the mean untreated potential outcome Y0Mean g t c, for every covariate cell c.
Formal statement
Proof (Lean source)
For finite sets of cohorts, periods, and covariate cells, a staggered-adoption cell system, a saturated untreated-outcome regression, a cohort, and a period, the imputation residual mean is the within-cohort covariate-weighted average of the observed cell mean minus the fitted untreated mean.
Definition (Lean source)
For finite sets of cohorts, periods, and covariate cells, a staggered-adoption cell system, a saturated untreated-outcome regression, a proposed cell coefficient, a cohort, and a period, the cell residual normal equation states that the within-cohort covariate-weighted mean of observed outcome minus fitted untreated outcome minus that coefficient is zero.
Definition (Lean source)
For finite sets of cohorts and periods, a cohort, and a period, the saturated treated-cell indicator is one at that cohort--period pair and zero at every other pair.
Definition (Lean source)
On top of a staggered-cell design P and its saturated untreated-outcome regression S, this structure packages three families of treated-cell coefficients — an imputation coefficient, a pooled-least-squares (POLS) coefficient, and an extended two-way-fixed-effects (ETWFE) coefficient — together with the conditions pinning them down: on every treated cell the imputation coefficient equals the covariate-weighted imputation residual mean, and the POLS and ETWFE coefficients each solve the finite-cell covariate-weighted residual normal equation.
Definition (Lean source)
POLS cell coefficients equal imputation. On any treated cohort-time cell (g,t), the flexible POLS cell coefficient equals the imputation residual mean at that cell.
Formal statement
Proof (Lean source)
ETWFE cell coefficients equal imputation. On any treated cohort-time cell (g,t), the extended two-way-fixed-effects (ETWFE) cell coefficient equals the imputation residual mean at that cell.
Formal statement
Proof (Lean source)
For finite sets of cohorts, periods, and covariate cells, a staggered-adoption cell system, a saturated untreated-outcome regression, a flexible-DID estimand collection, and a cohort-period weighting function, the aggregate imputation estimand is the weighted sum of imputation coefficients over treated cells.
Definition (Lean source)
For finite sets of cohorts, periods, and covariate cells, a staggered-adoption cell system, a saturated untreated-outcome regression, a flexible-DID estimand collection, and a cohort-period weighting function, the aggregate pooled-least-squares estimand is the weighted sum of pooled-least-squares coefficients over treated cells.
Definition (Lean source)
For finite sets of cohorts, periods, and covariate cells, a staggered-adoption cell system, a saturated untreated-outcome regression, a flexible-DID estimand collection, and a cohort-period weighting function, the aggregate extended two-way- fixed-effects estimand is the weighted sum of extended two-way-fixed- effects coefficients over treated cells.
Definition (Lean source)
Cell-level characterization: imputation, POLS, and ETWFE agree with the ATT cell. If no anticipation holds, conditional parallel trends holds — the mean untreated potential outcome admits an additive cohort/time fixed-effects representation given covariates, and (g,t) is a treated cohort-time cell covered by the untreated-regression witness S and the imputation/POLS/ETWFE estimands E, then the imputation, POLS, and ETWFE cell coefficients at (g,t) all equal the ATT cell τ_gt.
Formal statement
Proof (Lean source)
Aggregate characterization: every weighting of imputation, POLS, and ETWFE equals the weighted ATT aggregate. If no anticipation holds and conditional parallel trends holds — the mean untreated potential outcome admits an additive cohort/time fixed-effects representation given covariates, then for any treated-cell weighting function a, the a-weighted aggregates of the imputation, POLS, and ETWFE cell estimands all equal the a-weighted ATT aggregate.
Formal statement
Proof (Lean source)
Headline finite-cell characterization (Wooldridge, Theorem B). If no anticipation holds: the treated and untreated potential-outcome means agree on every cell in the untreated-outcome regression's design and conditional parallel trends holds — the mean untreated potential outcome admits an additive cohort/time fixed-effects representation given covariates, then, given the saturated untreated regression S and the POLS/ETWFE finite-cell residual normal equations carried by E, on every treated cohort-time cell the flexible imputation, POLS, and ETWFE estimands all equal the ATT cell, and consequently every treated-cell weighted aggregate of the three estimands equals the correspondingly weighted ATT aggregate.
Formal statement
Proof (Lean source)
6 supporting declarations (lemmas, instances)
-
untreatedFittheorem — The weighted projection m0 reproduces the factual cohort-g outcome mean on every untreated cell.hypothesesCohort :sharedType u_1Time :sharedType u_2S :hNA :NoAnticipation PhCPT :g :Cohortt :Timehgt :P.untreatedCell g tc :CovarconclusionS.m0 g t c = P.YgMean g t cProof (Lean source)
theorem untreatedFit {P : StaggeredATTCells Cohort Time Covar} (S : UntreatedFitWitness P) (hNA : NoAnticipation P) (hCPT : ConditionalParallelTrendsAdditive P) ⦃g : Cohort⦄ ⦃t : Time⦄ (hgt : P.untreatedCell g t) (c : Covar) : S.m0 g t c = P.YgMean g t c := by classical obtain ⟨αy, lamy, hy⟩ := hCPT obtain ⟨αm, lamm, hm⟩ := S.additive set d : Cohort → Time → Covar → ℝ := fun g t c => S.m0 g t c - P.Y0Mean g t c with hd have hd_add : IsCellAdditive (Cohort := Cohort) d := by refine ⟨fun g c => αm g c - αy g c, fun t c => lamm t c - lamy t c, ?_⟩ intro g t c simp only [hd, hm, hy]; ring have hne := S.untreatedNormalEq d hd_add -- The positively-weighted squared residual over the untreated design vanishes. have hsq : (∑ gt ∈ P.untreatedCells, ∑ c, S.untreatedWeight gt.1 gt.2 c * (d gt.1 gt.2 c) ^ 2) = 0 := by have hQR : (∑ gt ∈ P.untreatedCells, ∑ c, S.untreatedWeight gt.1 gt.2 c * (d gt.1 gt.2 c) ^ 2) + (∑ gt ∈ P.untreatedCells, ∑ c, S.untreatedWeight gt.1 gt.2 c * (P.observedMean gt.1 gt.2 c - S.m0 gt.1 gt.2 c) * d gt.1 gt.2 c) = 0 := by rw [← Finset.sum_add_distrib] refine Finset.sum_eq_zero ?_ intro gt hgt_mem have hut : P.untreatedCell gt.1 gt.2 := by simpa [StaggeredATTCells.untreatedCells] using hgt_mem rw [← Finset.sum_add_distrib] refine Finset.sum_eq_zero ?_ intro c _ have hobs : P.observedMean gt.1 gt.2 c = P.Y0Mean gt.1 gt.2 c := P.consistency_untreated hut c simp only [hd] rw [hobs]; ring linarith [hQR, hne] -- Extract the single untreated cell `(g,t)` and covariate `c`. have hmem : (g, t) ∈ P.untreatedCells := by simp only [StaggeredATTCells.untreatedCells, mem_filter, Finset.mem_univ, true_and] exact hgt have hrow_nonneg : ∀ gt ∈ P.untreatedCells, 0 ≤ ∑ c, S.untreatedWeight gt.1 gt.2 c * (d gt.1 gt.2 c) ^ 2 := by intro gt hgt_mem have hut : P.untreatedCell gt.1 gt.2 := by simpa [StaggeredATTCells.untreatedCells] using hgt_mem exact sum_nonneg fun c _ => mul_nonneg (le_of_lt (S.untreatedWeight_pos hut c)) (sq_nonneg _) have hrow := (Finset.sum_eq_zero_iff_of_nonneg hrow_nonneg).mp hsq (g, t) hmem have hcell_nonneg : ∀ c' ∈ (Finset.univ : Finset Covar), 0 ≤ S.untreatedWeight g t c' * (d g t c') ^ 2 := fun c' _ => mul_nonneg (le_of_lt (S.untreatedWeight_pos hgt c')) (sq_nonneg _) have hcell := (Finset.sum_eq_zero_iff_of_nonneg hcell_nonneg).mp hrow c (Finset.mem_univ c) have hw := S.untreatedWeight_pos hgt c have hd0 : d g t c = 0 := by have hsq0 : (d g t c) ^ 2 = 0 := (mul_eq_zero.mp hcell).resolve_left (ne_of_gt hw) exact pow_eq_zero_iff (by norm_num) |>.mp hsq0 have hm0 : S.m0 g t c = P.Y0Mean g t c := by have hh := hd0; simp only [hd] at hh; linarith rw [hm0]; exact (hNA hgt c).symm -
cellResidualNormalEq_eq_imputationThetatheorem — A finite-cell residual normal equation identifies the coefficient with the imputation residual mean.hypothesesCohort :sharedType u_1Time :sharedType u_2Covar :sharedType u_3outcome fitted :Cohort → Time → Covar → ℝcovarWeight :Cohort → Covar → ℝcovarWeight_sum_one :∀ g, ∑ c, covarWeight g c = 1theta :ℝg :Cohortt :Timehθ :∑ c, covarWeight g c * (outcome g t c - fitted g t c - theta) = 0conclusiontheta = ∑ c, covarWeight g c * (outcome g t c - fitted g t c)Proof (Lean source)
theorem cellResidualNormalEq_eq_imputationTheta (outcome fitted : Cohort → Time → Covar → ℝ) (covarWeight : Cohort → Covar → ℝ) (covarWeight_sum_one : ∀ g, ∑ c, covarWeight g c = 1) {theta : ℝ} {g : Cohort} {t : Time} (hθ : ∑ c, covarWeight g c * (outcome g t c - fitted g t c - theta) = 0) : theta = ∑ c, covarWeight g c * (outcome g t c - fitted g t c) := by have hsum : (∑ c, covarWeight g c * (outcome g t c - fitted g t c - theta)) = (∑ c, covarWeight g c * (outcome g t c - fitted g t c)) - (∑ c, covarWeight g c) * theta := by simp only [mul_sub, Finset.sum_sub_distrib, Finset.sum_mul] have hnormal : (∑ c, covarWeight g c * (outcome g t c - fitted g t c)) - theta = 0 := by calc (∑ c, covarWeight g c * (outcome g t c - fitted g t c)) - theta = (∑ c, covarWeight g c * (outcome g t c - fitted g t c)) - (∑ c, covarWeight g c) * theta := by rw [covarWeight_sum_one g] ring _ = ∑ c, covarWeight g c * (outcome g t c - fitted g t c - theta) := by rw [hsum] _ = 0 := hθ exact (sub_eq_zero.mp hnormal).symm -
cellIndicator_normalEq_eq_cellResidualtheorem — Saturated block-diagonalization for treated-cell indicators.hypothesesCohort :sharedType u_1Time :sharedType u_2Covar :sharedType u_3DecidableEq CohortDecidableEq Timeoutcome fitted :Cohort → Time → Covar → ℝcovarWeight :Cohort → Covar → ℝtheta :ℝg :Cohortt :Timeconclusion(∑ g', ∑ t', ∑ c, cellIndicator g t g' t' * covarWeight g' c * (outcome g' t' c - fitted g' t' c - cellIndicator g t g' t' * theta) = 0)↔ ∑ c, covarWeight g c * (outcome g t c - fitted g t c - theta) = 0Proof (Lean source)
theorem cellIndicator_normalEq_eq_cellResidual [DecidableEq Cohort] [DecidableEq Time] (outcome fitted : Cohort → Time → Covar → ℝ) (covarWeight : Cohort → Covar → ℝ) (theta : ℝ) (g : Cohort) (t : Time) : (∑ g', ∑ t', ∑ c, cellIndicator g t g' t' * covarWeight g' c * (outcome g' t' c - fitted g' t' c - cellIndicator g t g' t' * theta) = 0) ↔ ∑ c, covarWeight g c * (outcome g t c - fitted g t c - theta) = 0 := by classical unfold cellIndicator -- The full saturated sum collapses to the single-cell residual sum, because -- the saturated indicator vanishes off cell `(g,t)`. have hcollapse : (∑ g', ∑ t', ∑ c, (if g' = g ∧ t' = t then (1 : ℝ) else 0) * covarWeight g' c * (outcome g' t' c - fitted g' t' c - (if g' = g ∧ t' = t then (1 : ℝ) else 0) * theta)) = ∑ c, covarWeight g c * (outcome g t c - fitted g t c - theta) := by rw [Finset.sum_eq_single g, Finset.sum_eq_single t] · refine Finset.sum_congr rfl ?_ intro c _ simp · intro t' _ ht' refine Finset.sum_eq_zero ?_ intro c _ simp [ht'] · intro hg; simp at hg · intro g' _ hg' refine Finset.sum_eq_zero ?_ intro t' _ refine Finset.sum_eq_zero ?_ intro c _ simp [hg'] · intro hg; simp at hg rw [hcollapse] -
pols_cell_eq_imputationtheorem — Compatibility alias: the POLS/imputation equality is now derived from the POLS normal equation, rather than stored as a field.hypothesesCohort :sharedType u_1Time :sharedType u_2Covar :sharedType u_3P :StaggeredATTCells Cohort Time CovarE :g :Cohortt :Timehgt :P.treatedCell g tconclusionE.thetaPOLS g t = E.thetaImp g tProof (Lean source)
theorem pols_cell_eq_imputation (P : StaggeredATTCells Cohort Time Covar) (S : SaturatedUntreatedRegression P) (E : FlexibleDIDEstimands P S) {g : Cohort} {t : Time} (hgt : P.treatedCell g t) : E.thetaPOLS g t = E.thetaImp g t := by rw [E.thetaPOLS_eq_imputationTheta P S hgt, E.thetaImp_eq_imputation hgt] -
etwfe_cell_eq_polstheorem — Compatibility alias: ETWFE/POLS equality is now derived by solving both finite-cell normal equations, rather than stored as a field.hypothesesCohort :sharedType u_1Time :sharedType u_2Covar :sharedType u_3P :StaggeredATTCells Cohort Time CovarE :g :Cohortt :Timehgt :P.treatedCell g tconclusionE.thetaETWFE g t = E.thetaPOLS g tProof (Lean source)
theorem etwfe_cell_eq_pols (P : StaggeredATTCells Cohort Time Covar) (S : SaturatedUntreatedRegression P) (E : FlexibleDIDEstimands P S) {g : Cohort} {t : Time} (hgt : P.treatedCell g t) : E.thetaETWFE g t = E.thetaPOLS g t := by rw [E.thetaETWFE_eq_imputationTheta P S hgt, E.thetaPOLS_eq_imputationTheta P S hgt] -
imputationTheta_eq_tauCelltheorem — Imputation recovers the ATT cell once the saturated untreated prediction equals the untreated potential-outcome mean in target cells.hypothesesCohort :sharedType u_1Time :sharedType u_2Covar :sharedType u_3P :StaggeredATTCells Cohort Time CovarE :hNA :NoAnticipation PhCPT :g :Cohortt :Timehgt :P.treatedCell g tconclusionE.thetaImp g t = P.tauCell g tProof (Lean source)
theorem imputationTheta_eq_tauCell (P : StaggeredATTCells Cohort Time Covar) (S : SaturatedUntreatedRegression P) (E : FlexibleDIDEstimands P S) (hNA : NoAnticipation P) (hCPT : ConditionalParallelTrendsAdditive P) {g : Cohort} {t : Time} (hgt : P.treatedCell g t) : E.thetaImp g t = P.tauCell g t := by rw [E.thetaImp_eq_imputation hgt] unfold imputationTheta StaggeredATTCells.tauCell refine Finset.sum_congr rfl ?_ intro c _hc rw [P.consistency_treated hgt c, S.recovers_target_Y0 hNA hCPT hgt c]
TWFE 8 core · 5 supporting This file formalizes the scalar-regressor finite balanced-panel version of Wooldridge's two-way fixed effects and two-way Mundlak equivalence. ★ twfe_twm_equivalence
Wooldridge Scalar TWFE and Mundlak
This file formalizes the scalar-regressor finite balanced-panel version of
Wooldridge's two-way fixed effects and two-way Mundlak equivalence. It defines
the scalar TWFE problem, coefficient, and normal equation, proves
ScalarTWFEProblem.betaTWFE_normalEq and ScalarTWFEProblem.betaTWFE_unique, and
then proves twfe_twm_equivalence and
twfe_twm_optional_controls_invariant for coding-free two-way Mundlak fits.
A scalar two-way-fixed-effects regression problem on a finite balanced panel of units and time periods, given a scalar outcome and a scalar regressor, where the sum of squared double-demeaned regressor values is strictly positive — the scalar full-rank condition ensuring the two-way within estimator is well defined.
Definition (Lean source)
For finite sets of units and periods and a scalar two-way-fixed-effects regression problem, the residualized-design denominator is the sum of squared doubly demeaned regressor values over all unit--period observations.
Definition (Lean source)
For finite sets of units and periods and a scalar two-way-fixed-effects regression problem, the residualized numerator is the sum, over all unit--period observations, of the doubly demeaned regressor times the doubly demeaned outcome.
Definition (Lean source)
For finite sets of units and periods and a scalar two-way-fixed-effects regression problem, the scalar two-way-fixed- effects coefficient is the residualized numerator divided by the residualized-design denominator.
Definition (Lean source)
For finite sets of units and periods, a scalar two-way- fixed-effects regression problem, and a proposed coefficient, the scalar two-way-fixed-effects normal equation states that the sum of the doubly demeaned regressor times the corresponding residual is zero.
Definition (Lean source)
For finite sets of units, periods, unit-level controls, and period-level controls, a scalar regressor, unit-level control functions, period-level control functions, and a candidate nuisance function, the two-way Mundlak nuisance condition holds exactly when the candidate is a constant plus arbitrary multiples of the regressor's unit means and period means and linear combinations of the supplied unit-level and period-level controls.
Definition (Lean source)
A scalar two-way Mundlak fit of the TWFE problem P against optional time-constant controls Zvar and time-only controls Mvar, stated by normal equations rather than by a particular coding of the nuisance regressors. It bundles a scalar coefficient on the regressor and a nuisance function lying in the two-way Mundlak span, subject to the pooled normal equation against the regressor and the pooled normal equation against every nuisance function in that span.
Definition (Lean source)
Wooldridge finite-panel scalar TWFE-two-way-Mundlak equivalence. For a scalar two-way-fixed-effects panel regression problem P with optional time-constant controls Zvar and time-only controls Mvar, given any pooled two-way Mundlak regression fit stated by its normal equations, that fit's coefficient on the regressor equals the two-way-fixed-effects coefficient.
Formal statement
Proof (Lean source)
5 supporting declarations (lemmas, instances)
-
betaTWFE_normalEqtheorem — The closed-form coefficient satisfies the scalar TWFE normal equation by dividing through the positive residualized sum of squares.hypothesesconclusionP.twfeNormalEq P.betaTWFEProof (Lean source)
theorem betaTWFE_normalEq (P : ScalarTWFEProblem Unit Time) : P.twfeNormalEq P.betaTWFE := by let A : ℝ := ∑ i, ∑ t, ddot P.X i t * ddot P.Y i t let B : ℝ := ∑ i, ∑ t, (ddot P.X i t)^2 have hden : B ≠ 0 := by dsimp [B] exact ne_of_gt P.ddotX_ss_pos have hfactor : ∀ c : ℝ, (∑ i, ∑ t, ddot P.X i t * (ddot P.X i t * c)) = B * c := by intro c dsimp [B] simp only [← mul_assoc, pow_two, Finset.sum_mul] unfold twfeNormalEq betaTWFE twfeNumerator twfeDenominator change ∑ i, ∑ t, ddot P.X i t * (ddot P.Y i t - ddot P.X i t * (A / B)) = 0 calc ∑ i, ∑ t, ddot P.X i t * (ddot P.Y i t - ddot P.X i t * (A / B)) = A - B * (A / B) := by dsimp [A] simp only [mul_sub, Finset.sum_sub_distrib] rw [hfactor] _ = 0 := by rw [div_eq_mul_inv] rw [show B * (A * B⁻¹) = A * (B * B⁻¹) by ring] rw [mul_inv_cancel₀ hden] ring -
betaTWFE_uniquetheorem — Scalar full-rank uniqueness of the TWFE normal-equation solution.hypothesesUnit :sharedType u_1Time :sharedType u_2P :ScalarTWFEProblem Unit Timeβ :ℝhβ :P.twfeNormalEq βconclusionβ = P.betaTWFEProof (Lean source)
theorem betaTWFE_unique (P : ScalarTWFEProblem Unit Time) {β : ℝ} (hβ : P.twfeNormalEq β) : β = P.betaTWFE := by unfold twfeNormalEq at hβ change β = (∑ i, ∑ t, ddot P.X i t * ddot P.Y i t) / (∑ i, ∑ t, (ddot P.X i t)^2) have hden : (∑ i, ∑ t, (ddot P.X i t)^2) ≠ 0 := ne_of_gt P.ddotX_ss_pos have hnormal : (∑ i, ∑ t, ddot P.X i t * ddot P.Y i t) - (∑ i, ∑ t, (ddot P.X i t)^2) * β = 0 := by calc (∑ i, ∑ t, ddot P.X i t * ddot P.Y i t) - (∑ i, ∑ t, (ddot P.X i t)^2) * β = ∑ i, ∑ t, ddot P.X i t * (ddot P.Y i t - ddot P.X i t * β) := by simp only [mul_sub, Finset.sum_sub_distrib] ring_nf simp only [pow_two, Finset.sum_mul] simp [mul_comm] _ = 0 := hβ have hnum : (∑ i, ∑ t, ddot P.X i t * ddot P.Y i t) = (∑ i, ∑ t, (ddot P.X i t)^2) * β := sub_eq_zero.mp hnormal calc β = ((∑ i, ∑ t, (ddot P.X i t)^2) * β) / (∑ i, ∑ t, (ddot P.X i t)^2) := by rw [div_eq_mul_inv] rw [show ((∑ i, ∑ t, (ddot P.X i t)^2) * β) * (∑ i, ∑ t, (ddot P.X i t)^2)⁻¹ = β * ((∑ i, ∑ t, (ddot P.X i t)^2) * (∑ i, ∑ t, (ddot P.X i t)^2)⁻¹) by ring] rw [mul_inv_cancel₀ hden, mul_one] _ = (∑ i, ∑ t, ddot P.X i t * ddot P.Y i t) / (∑ i, ∑ t, (ddot P.X i t)^2) := by rw [← hnum] -
mundlak_nuisance_unit_timetheorem — Mundlak nuisance functions are unit/time additive, so optional time-constant and time-only controls lie inside the same orthogonality class.hypothesesUnit :sharedType u_1Time :sharedType u_2Z :sharedType u_3M :sharedType u_4X :Unit → Time → ℝZvar :Z → Unit → ℝMvar :M → Time → ℝh :Unit → Time → ℝhh :IsTwoWayMundlakNuisance X Zvar Mvar hconclusionIsUnitTimeAdditive hProof (Lean source)
theorem mundlak_nuisance_unit_time (X : Unit → Time → ℝ) (Zvar : Z → Unit → ℝ) (Mvar : M → Time → ℝ) {h : Unit → Time → ℝ} (hh : IsTwoWayMundlakNuisance X Zvar Mvar h) : IsUnitTimeAdditive h := by rcases hh with ⟨c, γu, γt, ζ, μ, hrep⟩ refine ⟨fun i => c + γu * unitMean X i + ∑ z, ζ z * Zvar z i, fun t => γt * timeMean X t + ∑ m, μ m * Mvar m t, ?_⟩ intro i t rw [hrep i t] ring -
twfe_twm_residual_commontheorem — Residualizing the scalar regressor against the two-way Mundlak nuisance span leaves the same residual as double demeaning.hypothesesUnit :sharedType u_1Time :sharedType u_2Z :sharedType u_3M :sharedType u_4P :ScalarTWFEProblem Unit TimeZvar :Z → Unit → ℝMvar :M → Time → ℝconclusionconclusion 1IsUnitTimeAdditive (fun i t => P.X i t - ddot P.X i t)Proof (Lean source)
theorem twfe_twm_residual_common (P : ScalarTWFEProblem Unit Time) (Zvar : Z → Unit → ℝ) (Mvar : M → Time → ℝ) : IsUnitTimeAdditive (fun i t => P.X i t - ddot P.X i t) ∧ (∀ h : Unit → Time → ℝ, IsTwoWayMundlakNuisance P.X Zvar Mvar h → inner (ddot P.X) h = 0) := by constructor · rw [show (fun i t => P.X i t - ddot P.X i t) = unitTimeProjection P.X by funext i t exact sub_ddot_eq_unitTimeProjection P.X i t] exact unitTimeProjection_additive P.X · intro h hh exact ddot_orthogonal_unit_time (lt_of_lt_of_le (by decide) P.panel.unit_card_ge_two) (lt_of_lt_of_le (by decide) P.panel.time_card_ge_two) P.X h (mundlak_nuisance_unit_time P.X Zvar Mvar hh) -
twfe_twm_optional_controls_invarianttheorem — Adding or removing optional time-constant or time-only controls does not change the scalar coefficient, because both fits equal the TWFE coefficient.hypothesesUnit :sharedType u_1Time :sharedType u_2P :ScalarTWFEProblem Unit TimeZvar₁ :Z₁ → Unit → ℝMvar₁ :M₁ → Time → ℝZvar₂ :Z₂ → Unit → ℝMvar₂ :M₂ → Time → ℝfit₁ :ScalarTWMFit P Zvar₁ Mvar₁fit₂ :ScalarTWMFit P Zvar₂ Mvar₂conclusionfit₁.beta = fit₂.betaProof (Lean source)
theorem twfe_twm_optional_controls_invariant {Z₁ M₁ Z₂ M₂ : Type*} [Fintype Z₁] [Fintype M₁] [Fintype Z₂] [Fintype M₂] (P : ScalarTWFEProblem Unit Time) (Zvar₁ : Z₁ → Unit → ℝ) (Mvar₁ : M₁ → Time → ℝ) (Zvar₂ : Z₂ → Unit → ℝ) (Mvar₂ : M₂ → Time → ℝ) (fit₁ : ScalarTWMFit P Zvar₁ Mvar₁) (fit₂ : ScalarTWMFit P Zvar₂ Mvar₂) : fit₁.beta = fit₂.beta := by rw [twfe_twm_equivalence P Zvar₁ Mvar₁ fit₁, twfe_twm_equivalence P Zvar₂ Mvar₂ fit₂]
VectorTWFE 9 core · 2 supporting This file defines the finite-dimensional vector-regressor version of Wooldridge's two-way fixed effects normal equation on a balanced panel. ★ betaTWFE_normalEq★ betaTWFE_unique
Wooldridge Vector TWFE
This file defines the finite-dimensional vector-regressor version of
Wooldridge's two-way fixed effects normal equation on a balanced panel. It
constructs the componentwise residual ddotVec, residualized Gram matrix
gram, numerator numer, and VectorTWFEProblem.betaTWFE. It proves
vecNormalEq_iff_mulVec, VectorTWFEProblem.betaTWFE_normalEq, and
VectorTWFEProblem.betaTWFE_unique, then relates the scalar problem to the
one-coordinate case with ScalarTWFEProblem.toVector and
ScalarTWFEProblem.toVector_betaTWFE.
For finite unit, time-period, and regressor-coordinate sets, a vector-valued regressor array, a unit, a time period, and a regressor coordinate, the componentwise double-demeaned regressor is the scalar double demean of that coordinate over the finite balanced panel.
Definition (Lean source)
For finite unit, time-period, and regressor-coordinate sets and a vector-valued regressor array, the residualized Gram matrix has entry equal to the finite sum, over units and time periods, of the product of the double-demeaned -th and -th regressor coordinates.
For finite unit, time-period, and regressor-coordinate sets, a vector-valued regressor array, and an outcome array, the residualized numerator vector has coordinate equal to the finite sum of the product of the double-demeaned -th regressor and the double-demeaned outcome.
Definition (Lean source)
A K-vector two-way-fixed-effects regression problem on a finite balanced panel of units and time periods, given a scalar outcome and a K-vector of regressors, where the residualized Gram matrix of the double-demeaned regressors is nonsingular — the vector full-rank condition ensuring the two-way within estimator is well defined.
Definition (Lean source)
For finite unit, time-period, and regressor-coordinate sets and a vector two-way-fixed-effects problem, the closed-form vector TWFE coefficient is the inverse residualized Gram matrix multiplied by the residualized outcome-regressor numerator vector.
Definition (Lean source)
For finite unit, time-period, and regressor-coordinate sets, a vector two-way-fixed-effects problem, and a candidate coefficient vector, the vector TWFE normal-equation condition requires that, for every regressor coordinate, the finite inner product of its double-demeaned regressor with the double-demeaned outcome residual is zero.
Definition (Lean source)
Existence of a TWFE solution. For a vector two-way-fixed-effects problem, whose residualized Gram matrix is nonsingular by assumption, the closed-form coefficient P.betaTWFE solves the matrix normal equation defining the TWFE coefficient.
Formal statement
Proof (Lean source)
Full-rank uniqueness of the vector TWFE coefficient. For a vector TWFE problem P with nonsingular residualized Gram matrix, if a coefficient vector β satisfies the coordinate-wise TWFE normal equation — in every coordinate the double-demeaned regressor is orthogonal to the double-demeaned residual, then β equals the closed-form vector TWFE coefficient P.betaTWFE.
Formal statement
Proof (Lean source)
For finite unit and time-period sets and a scalar two-way-fixed-effects problem, the associated one-coordinate vector two-way-fixed-effects problem has the same panel and outcome, uses the scalar regressor as its sole coordinate, and has a nonsingular residualized Gram matrix because the scalar double-demeaned regressor has a strictly positive sum of squares.
Definition (Lean source)
2 supporting declarations (lemmas, instances)
-
vecNormalEq_iff_mulVectheorem — The coordinate-wise normal equation is equivalent to the matrix normal equation Q_{\ddot X} β = Σ_it ddot X ddot Y.hypothesesUnit :sharedType u_1Time :sharedType u_2K :sharedType u_3X :Unit → Time → K → ℝY :Unit → Time → ℝβ :K → ℝProof (Lean source)
theorem vecNormalEq_iff_mulVec (X : Unit → Time → K → ℝ) (Y : Unit → Time → ℝ) (β : K → ℝ) : (∀ k, ∑ i, ∑ t, ddotVec X i t k * (ddot Y i t - ∑ j, ddotVec X i t j * β j) = 0) ↔ (gram X).mulVec β = numer X Y := by have key : ∀ k, ∑ i, ∑ t, ddotVec X i t k * (ddot Y i t - ∑ j, ddotVec X i t j * β j) = numer X Y k - (gram X).mulVec β k := by intro k have hmv : (gram X).mulVec β k = ∑ j, (∑ i, ∑ t, ddotVec X i t k * ddotVec X i t j) * β j := by simp only [mulVec, dotProduct, gram] rw [hmv] change ∑ i, ∑ t, ddotVec X i t k * (ddot Y i t - ∑ j, ddotVec X i t j * β j) = (∑ i, ∑ t, ddotVec X i t k * ddot Y i t) - ∑ j, (∑ i, ∑ t, ddotVec X i t k * ddotVec X i t j) * β j -- split off the regressor term and swap the `j` sum outward have hsplit : ∑ i, ∑ t, ddotVec X i t k * (ddot Y i t - ∑ j, ddotVec X i t j * β j) = (∑ i, ∑ t, ddotVec X i t k * ddot Y i t) - ∑ i, ∑ t, ∑ j, ddotVec X i t k * ddotVec X i t j * β j := by rw [← Finset.sum_sub_distrib] refine Finset.sum_congr rfl (fun i _ => ?_) rw [← Finset.sum_sub_distrib] refine Finset.sum_congr rfl (fun t _ => ?_) rw [mul_sub, Finset.mul_sum] congr 1 refine Finset.sum_congr rfl (fun j _ => ?_) ring rw [hsplit] congr 1 -- reorder ∑ i ∑ t ∑ j → ∑ j ∑ i ∑ t and pull `β j` out of the i,t sums calc ∑ i, ∑ t, ∑ j, ddotVec X i t k * ddotVec X i t j * β j = ∑ i, ∑ j, ∑ t, ddotVec X i t k * ddotVec X i t j * β j := by refine Finset.sum_congr rfl (fun i _ => ?_) rw [Finset.sum_comm] _ = ∑ j, ∑ i, ∑ t, ddotVec X i t k * ddotVec X i t j * β j := by rw [Finset.sum_comm] _ = ∑ j, (∑ i, ∑ t, ddotVec X i t k * ddotVec X i t j) * β j := by refine Finset.sum_congr rfl (fun j _ => ?_) rw [Finset.sum_mul] refine Finset.sum_congr rfl (fun i _ => ?_) rw [Finset.sum_mul] constructor · intro h funext k have := key k rw [h k] at this -- 0 = numer k - mulVec k ⇒ mulVec k = numer k linarith [this] · intro h k rw [key k, h] ring -
toVector_betaTWFEtheorem — The singleton-coordinate vector TWFE coefficient recovers the scalar TWFE coefficient, so the scalar theorem is the K = Fin 1 case of the vector one.hypothesesconclusionP.toVector.betaTWFE 0 = P.betaTWFEProof (Lean source)
theorem ScalarTWFEProblem.toVector_betaTWFE (P : ScalarTWFEProblem Unit Time) : P.toVector.betaTWFE 0 = P.betaTWFE := by have hsol : P.toVector.vecTwfeNormalEq (fun _ => P.betaTWFE) := by intro k have h := P.betaTWFE_normalEq rw [ScalarTWFEProblem.twfeNormalEq] at h simpa [VectorTWFEProblem.vecTwfeNormalEq, ScalarTWFEProblem.toVector, ddotVec, Fin.sum_univ_one] using h have heq := P.toVector.betaTWFE_unique hsol rw [← heq]
PopulationBridge 1 core · 3 supporting This file connects Wooldridge's finite imputation estimands to population conditional expectations. ★ thetaImp_eq_eventCondExp
Wooldridge Population Bridge
This file connects Wooldridge's finite imputation estimands to population
conditional expectations. The main bridges are
imputationTheta_eq_eventCondExp and thetaImp_eq_eventCondExp, which apply the
finite-partition law of iterated expectations to identify covariate-weighted
finite residual means with event-level conditional expectations. The companion
lemmas m0_eq_eventCondExp_treated and m0_eq_eventCondExp_untreated state the
population conditional-expectation origin of the saturated untreated fit on
treated and untreated cells.
The imputation estimand equals a population conditional expectation. On a treated cohort-time cell (g,t), suppose the cohort event is measurable, each covariate cell is measurable, the covariate cells are pairwise disjoint, the covariate cells cover the whole sample space, the treatment-effect integrand Δ is integrable, each finite covariate weight equals the conditional probability of that covariate cell given the cohort event, and each finite cell residual — the observed mean minus the fitted untreated mean — equals the within-cell conditional mean of Δ given the cohort event and that covariate cell. Then the imputation cell estimand thetaImp g t equals the population conditional expectation E[Δ | cohortEvent].
Formal statement
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
imputationTheta_eq_eventCondExptheorem — The finite imputation residual mean equals a population conditional expectation.hypothesesCohort :sharedType u_1Time :sharedType u_2Covar :sharedType u_3Ω :Type*μ :P :StaggeredATTCells Cohort Time Covarg :Cohortt :TimecohortEvent :Set ΩcovarCell :Covar → Set ΩΔ :Ω → ℝhG :MeasurableSet cohortEventhC :∀ c, MeasurableSet (covarCell c)hcov :(⋃ c, covarCell c) = univhΔ :Integrable Δ μhcell :∀ c, P.observedMean g t c - S.m0 g t c = eventCondExp μ (cohortEvent ∩ covarCell c) ΔconclusionimputationTheta P S g t = eventCondExp μ cohortEvent ΔProof (Lean source)
theorem imputationTheta_eq_eventCondExp {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsFiniteMeasure μ] (P : StaggeredATTCells Cohort Time Covar) (S : SaturatedUntreatedRegression P) (g : Cohort) (t : Time) (cohortEvent : Set Ω) (covarCell : Covar → Set Ω) (Δ : Ω → ℝ) (hG : MeasurableSet cohortEvent) (hC : ∀ c, MeasurableSet (covarCell c)) (hdisj : Pairwise (onFun Disjoint covarCell)) (hcov : (⋃ c, covarCell c) = univ) (hΔ : Integrable Δ μ) (hweight : ∀ c, P.covarWeight g c = (μ (cohortEvent ∩ covarCell c)).toReal / (μ cohortEvent).toReal) (hcell : ∀ c, P.observedMean g t c - S.m0 g t c = eventCondExp μ (cohortEvent ∩ covarCell c) Δ) : imputationTheta P S g t = eventCondExp μ cohortEvent Δ := by unfold imputationTheta rw [eventCondExp_eq_sum_condProb_mul_eventCondExp μ cohortEvent covarCell hG hC hdisj hcov (fun c => measure_ne_top μ (cohortEvent ∩ covarCell c)) Δ hΔ] refine Finset.sum_congr rfl (fun c _ => ?_) rw [hweight c, hcell c] -
m0_eq_eventCondExp_treatedtheorem — On a treated cell, the fitted untreated mean equals the population conditional mean of the untreated potential outcome.hypothesesCohort :sharedType u_1Time :sharedType u_2Covar :sharedType u_3Ω :Type*μ :Measure ΩP :StaggeredATTCells Cohort Time CovarhNA :NoAnticipation PhCPT :g :Cohortt :Timehgt :P.treatedCell g tc :CovarcellEvent :Cohort → Time → Covar → Set ΩY0pop :Ω → ℝhY0 :P.Y0Mean g t c = eventCondExp μ (cellEvent g t c) Y0popconclusionS.m0 g t c = eventCondExp μ (cellEvent g t c) Y0popProof (Lean source)
theorem m0_eq_eventCondExp_treated {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) {P : StaggeredATTCells Cohort Time Covar} (S : SaturatedUntreatedRegression P) (hNA : NoAnticipation P) (hCPT : ConditionalParallelTrendsAdditive P) {g : Cohort} {t : Time} (hgt : P.treatedCell g t) (c : Covar) (cellEvent : Cohort → Time → Covar → Set Ω) (Y0pop : Ω → ℝ) (hY0 : P.Y0Mean g t c = eventCondExp μ (cellEvent g t c) Y0pop) : S.m0 g t c = eventCondExp μ (cellEvent g t c) Y0pop := by rw [S.recovers_target_Y0 hNA hCPT hgt c, hY0] -
m0_eq_eventCondExp_untreatedtheorem — On an untreated cell, the fitted untreated mean equals the population conditional mean of the untreated potential outcome.hypothesesCohort :sharedType u_1Time :sharedType u_2Covar :sharedType u_3Ω :Type*μ :Measure ΩP :StaggeredATTCells Cohort Time CovarhNA :NoAnticipation PhCPT :g :Cohortt :Timehut :P.untreatedCell g tc :CovarcellEvent :Cohort → Time → Covar → Set ΩY0pop :Ω → ℝhY0 :P.Y0Mean g t c = eventCondExp μ (cellEvent g t c) Y0popconclusionS.m0 g t c = eventCondExp μ (cellEvent g t c) Y0popProof (Lean source)
theorem m0_eq_eventCondExp_untreated {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) {P : StaggeredATTCells Cohort Time Covar} (S : SaturatedUntreatedRegression P) (hNA : NoAnticipation P) (hCPT : ConditionalParallelTrendsAdditive P) {g : Cohort} {t : Time} (hut : P.untreatedCell g t) (c : Covar) (cellEvent : Cohort → Time → Covar → Set Ω) (Y0pop : Ω → ℝ) (hY0 : P.Y0Mean g t c = eventCondExp μ (cellEvent g t c) Y0pop) : S.m0 g t c = eventCondExp μ (cellEvent g t c) Y0pop := by have hfit := SaturatedUntreatedRegression.untreatedFit S.toUntreatedFitWitness hNA hCPT hut c rw [show S.m0 g t c = P.YgMean g t c by simpa [SaturatedUntreatedRegression.toUntreatedFitWitness] using hfit, hNA hut c, hY0]
PopulationOrigin 4 core · 0 supporting This file constructs the finite staggered-DID cell system from an underlying probability model. ★ ofPopulation★ m0_eq_eventCondExp_treated_ofPopulation★ m0_eq_eventCondExp_untreated_ofPopulation
Wooldridge Population Origin
This file constructs the finite staggered-DID cell system from an underlying
probability model. StaggeredATTCells.ofPopulation defines the cell means as
raw event-level quotients of population outcomes and derives the consistency
fields from pointwise potential-outcome consistency on the corresponding cells.
The corollaries m0_eq_eventCondExp_treated_ofPopulation and
m0_eq_eventCondExp_untreated_ofPopulation specialize the population bridge for
systems built by this constructor, so the untreated-fit identification
hypothesis is definitional.
For finite cohort, time-period, and covariate sets, a measurable sample space with a measure, cohort-time-covariate cell events, untreated, cohort-specific, and observed population outcome functions, treated and untreated cell indicators, cohort shares, and within-cohort covariate weights, if every cell event is measurable, every cell has strictly positive measure, each of the three outcome functions is integrable on every cell, cohort shares are strictly positive on treated cells, covariate weights are nonnegative and sum to one within every cohort, and the observed outcome agrees pointwise with the cohort-specific outcome on treated cells and with the untreated outcome on untreated cells, the finite staggered-DID cell system uses the supplied shares, weights, and indicators and defines each outcome mean as its population event-conditional mean.
Definition (Lean source)
For finite cohort, time-period, and covariate sets, a measurable sample space with a probability measure, cohort-time-covariate cell events, untreated, cohort-specific, and observed population outcome functions, treated and untreated cell indicators, cohort shares, and within-cohort covariate weights, if every cell event is measurable, every cell has strictly positive probability, each outcome function is integrable on every cell, cohort shares are strictly positive on treated cells, covariate weights are nonnegative and sum to one within every cohort, and pointwise consistency holds on treated and untreated cells, the finite staggered-DID cell system is the system constructed from the same data by the measure-based constructor.
Definition (Lean source)
On a treated cell in a population-built system, the fitted untreated mean equals the population conditional mean of the untreated potential outcome. Fix a population model on a sample space Ω, with population outcomes Y0pop, Ygpop, Yobspop; suppose every cell event cellEvent g t c is measurable, every cell has strictly positive probability mass, and the three population outcomes are each integrable on every cell. Suppose also the cohort share is strictly positive on every treated cell, the covariate weights are nonnegative and sum to one within each cohort, and the observed outcome agrees pointwise with the cohort-g outcome on treated cells and with the untreated outcome on untreated cells (pointwise consistency). If the finite cell system P is exactly the one built from this population data by StaggeredATTCells.ofPopulation and, for a saturated untreated regression S on P, no anticipation holds and conditional parallel trends holds, then on any treated cell (g,t), the saturated regression's fitted value S.m0 g t c equals the population conditional mean E[Y0pop | cellEvent g t c], for every covariate cell c.
Formal statement
Proof (Lean source)
On an untreated cell in a population-built system, the fitted untreated mean equals the population conditional mean of the untreated potential outcome. Fix a population model on a sample space Ω, with population outcomes Y0pop, Ygpop, Yobspop; suppose every cell event cellEvent g t c is measurable, every cell has strictly positive probability mass, and the three population outcomes are each integrable on every cell. Suppose also the cohort share is strictly positive on every treated cell, the covariate weights are nonnegative and sum to one within each cohort, and the observed outcome agrees pointwise with the cohort-g outcome on treated cells and with the untreated outcome on untreated cells (pointwise consistency). If the finite cell system P is exactly the one built from this population data by StaggeredATTCells.ofPopulation and, for a saturated untreated regression S on P, no anticipation holds and conditional parallel trends holds, then on any untreated cell (g,t), the saturated regression's fitted value S.m0 g t c equals the population conditional mean E[Y0pop | cellEvent g t c], for every covariate cell c.
Formal statement
Proof (Lean source)
VectorMundlak 5 core · 7 supporting This file extends the finite balanced-panel Mundlak equivalence from one regressor to a finite vector of regressors. ★ vec_twfe_twm_equivalence
Wooldridge Vector Mundlak Equivalence
This file extends the finite balanced-panel Mundlak equivalence from one
regressor to a finite vector of regressors. It defines the generic residualized
gramOf and numerOf, proves the matrix Frisch-Waugh-Lovell handoff
matrix_fwl_eq_of_normalEqs, introduces the vector two-way Mundlak nuisance span
and fit, and proves vec_twfe_twm_equivalence together with the optional-control
invariance theorem vec_twfe_twm_optional_controls_invariant.
For finite sets of units, periods, and regressor coordinates and a residualized vector regressor, the residualized Gram matrix has as its coordinate pair entry the sum over unit--period observations of the product of the corresponding two regressor coordinates.
Definition (Lean source)
For finite sets of units, periods, and regressor coordinates, a residualized vector regressor, and a residualized outcome, the residualized numerator vector has as each coordinate the sum over unit--period observations of that regressor coordinate times the outcome.
Definition (Lean source)
For finite sets of units, periods, regressor coordinates, unit-level controls, and period-level controls, a vector regressor, unit-level control functions, period-level control functions, and a candidate nuisance function, the vector two-way Mundlak nuisance condition holds exactly when the candidate is a constant plus linear combinations of every regressor coordinate's unit and period means and of the supplied unit-level and period-level controls.
Definition (Lean source)
A coding-free K-vector two-way Mundlak fit of the vector TWFE problem P against optional time-constant controls Zvar and time-only controls Mvar, stated by normal equations rather than by a particular coding of the nuisance regressors. It bundles a coefficient vector and a nuisance function lying in the vector two-way Mundlak span, subject to the pooled normal equation against every regressor coordinate and the pooled normal equation against every nuisance function in that span.
Definition (Lean source)
Wooldridge finite-panel K-vector TWFE-two-way-Mundlak equivalence (Theorem A). For a K-vector two-way-fixed-effects panel regression problem P with optional time-constant controls Zvar and time-only controls Mvar, given any pooled two-way Mundlak regression fit stated by its normal equations, that fit's coefficient vector on the regressors equals the K-vector two-way-fixed-effects coefficient vector.
Formal statement
Proof (Lean source)
7 supporting declarations (lemmas, instances)
-
gram_eq_gramOftheorem — gram is the residualized instance of the generic version.hypothesesUnit :sharedType u_1Time :sharedType u_2K :sharedType u_3X :Unit → Time → K → ℝProof (Lean source)
-
numer_eq_numerOftheorem — numer is the residualized instance of the generic version.hypothesesUnit :sharedType u_1Time :sharedType u_2K :sharedType u_3X :Unit → Time → K → ℝY :Unit → Time → ℝ -
sum_dotRegressortheorem — Reshuffle: a residualized regressor against a β-combination of regressors factors through the cross-Gram.hypothesesUnit :sharedType u_1Time :sharedType u_2K :sharedType u_3Dt D :Unit → Time → K → ℝβ :K → ℝk :Kconclusion(∑ i, ∑ t, Dt i t k * (∑ j, D i t j * β j)) = ∑ j, (∑ i, ∑ t, Dt i t k * D i t j) * β jProof (Lean source)
theorem sum_dotRegressor (Dt D : Unit → Time → K → ℝ) (β : K → ℝ) (k : K) : (∑ i, ∑ t, Dt i t k * (∑ j, D i t j * β j)) = ∑ j, (∑ i, ∑ t, Dt i t k * D i t j) * β j := by calc ∑ i, ∑ t, Dt i t k * (∑ j, D i t j * β j) = ∑ i, ∑ t, ∑ j, Dt i t k * D i t j * β j := by refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun t _ => ?_)) rw [Finset.mul_sum] refine Finset.sum_congr rfl (fun j _ => ?_) ring _ = ∑ i, ∑ j, ∑ t, Dt i t k * D i t j * β j := by refine Finset.sum_congr rfl (fun i _ => ?_) rw [Finset.sum_comm] _ = ∑ j, ∑ i, ∑ t, Dt i t k * D i t j * β j := by rw [Finset.sum_comm] _ = ∑ j, (∑ i, ∑ t, Dt i t k * D i t j) * β j := by refine Finset.sum_congr rfl (fun j _ => ?_) rw [Finset.sum_mul] refine Finset.sum_congr rfl (fun i _ => ?_) rw [Finset.sum_mul] -
matrix_fwl_eq_of_normalEqstheorem — Matrix Frisch-Waugh-Lovell handoff. If a coefficient vector β and nuisance term Hβ satisfy the finite normal equations against the raw vector regressor D and a nuisance class H, while each coordinate of the residualized regressor Dtilde is orthogonal to H and the residualized Gram matrix is nonsingular, then β is the residualized matrix coefficient.hypothesesUnit :sharedType u_1Time :sharedType u_2K :sharedType u_3H :(Unit → Time → ℝ) → PropY Yproj Ytilde :Unit → Time → ℝD Dproj Dtilde :Unit → Time → K → ℝHβ :Unit → Time → ℝβ :K → ℝhY :∀ i t, Y i t = Yproj i t + Ytilde i thD :∀ i t k, D i t k = Dproj i t k + Dtilde i t khDproj_mem :∀ k, H (fun i t => Dproj i t k)hHβ_mem :H HβhDtilde_orth :∀ k, ∀ h : Unit → Time → ℝ, H h → (∑ i, ∑ t, Dtilde i t k * h i t) = 0hYproj_orth :∀ k, (∑ i, ∑ t, Dtilde i t k * Yproj i t) = 0h_normal_D :∀ k, (∑ i, ∑ t, D i t k * (Y i t - (∑ j, D i t j * β j) - Hβ i t)) = 0h_normal_H :∀ h : Unit → Time → ℝifH hthen(∑ i, ∑ t, h i t * (Y i t - (∑ j, D i t j * β j) - Hβ i t)) = 0Proof (Lean source)
theorem matrix_fwl_eq_of_normalEqs (H : (Unit → Time → ℝ) → Prop) {Y Yproj Ytilde : Unit → Time → ℝ} {D Dproj Dtilde : Unit → Time → K → ℝ} {Hβ : Unit → Time → ℝ} {β : K → ℝ} (hY : ∀ i t, Y i t = Yproj i t + Ytilde i t) (hD : ∀ i t k, D i t k = Dproj i t k + Dtilde i t k) (hDproj_mem : ∀ k, H (fun i t => Dproj i t k)) (hHβ_mem : H Hβ) (hDtilde_orth : ∀ k, ∀ h : Unit → Time → ℝ, H h → (∑ i, ∑ t, Dtilde i t k * h i t) = 0) (hYproj_orth : ∀ k, (∑ i, ∑ t, Dtilde i t k * Yproj i t) = 0) (hgram_unit : IsUnit (gramOf Dtilde).det) (h_normal_D : ∀ k, (∑ i, ∑ t, D i t k * (Y i t - (∑ j, D i t j * β j) - Hβ i t)) = 0) (h_normal_H : ∀ h : Unit → Time → ℝ, H h → (∑ i, ∑ t, h i t * (Y i t - (∑ j, D i t j * β j) - Hβ i t)) = 0) : β = (gramOf Dtilde)⁻¹.mulVec (numerOf Dtilde Ytilde) := by -- residual `e` set e : Unit → Time → ℝ := fun i t => Y i t - (∑ j, D i t j * β j) - Hβ i t with he -- step 1: each residualized coordinate is orthogonal to the residual have hDt_e : ∀ k, (∑ i, ∑ t, Dtilde i t k * e i t) = 0 := by intro k have h1 : (∑ i, ∑ t, D i t k * e i t) = 0 := h_normal_D k have h2 : (∑ i, ∑ t, Dproj i t k * e i t) = 0 := h_normal_H _ (hDproj_mem k) have hsplit : (∑ i, ∑ t, D i t k * e i t) = (∑ i, ∑ t, Dproj i t k * e i t) + (∑ i, ∑ t, Dtilde i t k * e i t) := by rw [← Finset.sum_add_distrib] refine Finset.sum_congr rfl (fun i _ => ?_) rw [← Finset.sum_add_distrib] refine Finset.sum_congr rfl (fun t _ => ?_) rw [hD i t k]; ring linarith [h1, h2, hsplit] -- step 2: expand the orthogonality into the matrix normal equation have hexp : ∀ k, (∑ i, ∑ t, Dtilde i t k * e i t) = numerOf Dtilde Ytilde k - (gramOf Dtilde).mulVec β k := by intro k have hmv : (gramOf Dtilde).mulVec β k = ∑ j, (∑ i, ∑ t, Dtilde i t k * Dtilde i t j) * β j := by simp only [mulVec, dotProduct, gramOf] -- cellwise split of `Dtilde·k * e` have hcell : ∀ i t, Dtilde i t k * e i t = Dtilde i t k * Yproj i t + Dtilde i t k * Ytilde i t - Dtilde i t k * (∑ j, D i t j * β j) - Dtilde i t k * Hβ i t := by intro i t simp only [he] rw [hY i t]; ring have hsum4 : (∑ i, ∑ t, Dtilde i t k * e i t) = (∑ i, ∑ t, Dtilde i t k * Yproj i t) + (∑ i, ∑ t, Dtilde i t k * Ytilde i t) - (∑ i, ∑ t, Dtilde i t k * (∑ j, D i t j * β j)) - (∑ i, ∑ t, Dtilde i t k * Hβ i t) := by have hcong : (∑ i, ∑ t, Dtilde i t k * e i t) = ∑ i, ∑ t, (Dtilde i t k * Yproj i t + Dtilde i t k * Ytilde i t - Dtilde i t k * (∑ j, D i t j * β j) - Dtilde i t k * Hβ i t) := Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun t _ => hcell i t)) rw [hcong] simp only [Finset.sum_sub_distrib, Finset.sum_add_distrib] -- the `D·β` cross term factors through the residualized Gram (cross terms vanish) have hDj : ∀ j, (∑ i, ∑ t, Dtilde i t k * D i t j) = ∑ i, ∑ t, Dtilde i t k * Dtilde i t j := by intro j have horth : (∑ i, ∑ t, Dtilde i t k * Dproj i t j) = 0 := hDtilde_orth k (fun i t => Dproj i t j) (hDproj_mem j) calc (∑ i, ∑ t, Dtilde i t k * D i t j) = (∑ i, ∑ t, Dtilde i t k * Dproj i t j) + (∑ i, ∑ t, Dtilde i t k * Dtilde i t j) := by rw [← Finset.sum_add_distrib] refine Finset.sum_congr rfl (fun i _ => ?_) rw [← Finset.sum_add_distrib] refine Finset.sum_congr rfl (fun t _ => ?_) rw [hD i t j]; ring _ = ∑ i, ∑ t, Dtilde i t k * Dtilde i t j := by rw [horth]; ring have hjsum : (∑ j, (∑ i, ∑ t, Dtilde i t k * D i t j) * β j) = ∑ j, (∑ i, ∑ t, Dtilde i t k * Dtilde i t j) * β j := Finset.sum_congr rfl (fun j _ => by rw [hDj j]) rw [hsum4, hmv, hYproj_orth k, hDtilde_orth k Hβ hHβ_mem, sum_dotRegressor Dtilde D β k, hjsum] unfold numerOf ring -- assemble: gramOf.mulVec β = numerOf have hmatrix : (gramOf Dtilde).mulVec β = numerOf Dtilde Ytilde := by funext k have := hexp k rw [hDt_e k] at this linarith [this] -- invert rw [← hmatrix, Matrix.mulVec_mulVec, Matrix.nonsing_inv_mul _ hgram_unit, Matrix.one_mulVec] -
vector_mundlak_nuisance_unit_timetheorem — Vector two-way Mundlak nuisance terms are unit/time additive, so the optional controls lie inside the same orthogonality class as for the scalar case.hypothesesUnit :sharedType u_1Time :sharedType u_2K :sharedType u_3Z :sharedType u_4M :sharedType u_5X :Unit → Time → K → ℝZvar :Z → Unit → ℝMvar :M → Time → ℝh :Unit → Time → ℝhh :IsVectorTwoWayMundlakNuisance X Zvar Mvar hconclusionIsUnitTimeAdditive hProof (Lean source)
theorem vector_mundlak_nuisance_unit_time (X : Unit → Time → K → ℝ) (Zvar : Z → Unit → ℝ) (Mvar : M → Time → ℝ) {h : Unit → Time → ℝ} (hh : IsVectorTwoWayMundlakNuisance X Zvar Mvar h) : IsUnitTimeAdditive h := by rcases hh with ⟨c, γu, γt, ζ, μ, hrep⟩ refine ⟨fun i => c + (∑ k, γu k * unitMean (fun i t => X i t k) i) + ∑ z, ζ z * Zvar z i, fun t => (∑ k, γt k * timeMean (fun i t => X i t k) t) + ∑ m, μ m * Mvar m t, ?_⟩ intro i t rw [hrep i t]; ring -
sum_ite_one_multheorem — Selecting a single coordinate via a 0/1 indicator collapses the coordinate sum to that coordinate's value.hypothesesK :sharedType u_3k :Kf :K → ℝconclusion(∑ k', (if k' = k then (1 : ℝ) else 0) * f k') = f kProof (Lean source)
theorem sum_ite_one_mul (k : K) (f : K → ℝ) : (∑ k', (if k' = k then (1 : ℝ) else 0) * f k') = f k := by rw [Finset.sum_eq_single k] · simp · intro k' _ hne; simp [hne] · intro h; exact absurd (Finset.mem_univ k) h -
vec_twfe_twm_optional_controls_invarianttheorem — Adding or removing optional time-constant or time-only controls does not change the K-vector Mundlak coefficient, since both fits equal the vector TWFE coefficient.hypothesesUnit :sharedType u_1Time :sharedType u_2K :sharedType u_3P :VectorTWFEProblem Unit Time KZvar₁ :Z₁ → Unit → ℝMvar₁ :M₁ → Time → ℝZvar₂ :Z₂ → Unit → ℝMvar₂ :M₂ → Time → ℝfit₁ :VectorTWMFit P Zvar₁ Mvar₁fit₂ :VectorTWMFit P Zvar₂ Mvar₂conclusionfit₁.beta = fit₂.betaProof (Lean source)
theorem vec_twfe_twm_optional_controls_invariant {Z₁ M₁ Z₂ M₂ : Type*} [Fintype Z₁] [Fintype M₁] [Fintype Z₂] [Fintype M₂] (P : VectorTWFEProblem Unit Time K) (Zvar₁ : Z₁ → Unit → ℝ) (Mvar₁ : M₁ → Time → ℝ) (Zvar₂ : Z₂ → Unit → ℝ) (Mvar₂ : M₂ → Time → ℝ) (fit₁ : VectorTWMFit P Zvar₁ Mvar₁) (fit₂ : VectorTWMFit P Zvar₂ Mvar₂) : fit₁.beta = fit₂.beta := by rw [vec_twfe_twm_equivalence P Zvar₁ Mvar₁ fit₁, vec_twfe_twm_equivalence P Zvar₂ Mvar₂ fit₂]