Panel.EstimandCharacterization.FlexibleDIDMundlak
Wooldridge's extended TWFE: the equivalence of pooled OLS with saturated interactions and imputation-style estimands.
DID 23 core · 9 supporting This file provides finite-cell primitives for Wooldridge-style flexible imputation, pooled least squares, and extended two-way fixed effects difference-in-differences calculations. ★ thetaPOLS_eq_imputationTheta_of_normalEq★ thetaETWFE_eq_imputationTheta_of_normalEq★ flexible_did_scaffold_consequences
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 calculations. It takes the treated and untreated
cohort-period cells as arbitrary predicates, rather than deriving them from an
adoption process. It defines cell means, support conditions, untreated-outcome
regressions, normal-equation-based POLS/ETWFE coefficient candidates, and
weighted linear aggregates of cell effects. The main
public theorem is flexible_did_scaffold_consequences, which records the
algebraic consequences of supplying the estimator-specific normal equations;
the file does not construct POLS or ETWFE regressions from design matrices.
Finite cohort-period cell scaffold: 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 finite 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 finite 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 finite cell system, a cohort, and a period, the cell treatment-effect contrast is the covariate-weighted average, within that cohort, of the cohort-specific potential outcome minus the untreated potential outcome in that period. Its treatment interpretation requires the system's supplied treated-cell predicate to represent an actual treatment design.
Definition (Lean source)
The weighted linear aggregate of treated-cell effects for a finite cell system uses an arbitrary cohort-period coefficient function over finite cohort, period, and covariate sets. The coefficients need not be nonnegative or sum to one, so this definition alone carries no average-effect interpretation.
Definition (Lean source)
An aggregate-weight specification for a finite cell system over finite cohort, period, and covariate sets consists of cohort-period weights that are nonnegative on treated cells and sum to one across those cells.
Definition (Lean source)
For finite sets of cohorts, periods, and covariate cells and a finite cell system, the condition called 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 finite 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 finite 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 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)
An untreated-fit witness for a finite cohort-period cell system over finite cohort, period, and covariate sets consists of an additive fitted mean, untreated-cell weights that are strictly positive on the untreated design, and weighted normal equations against every additive test function.
Definition (Lean source)
For finite sets of cohorts, periods, and covariate cells, the finite 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)
For finite sets of cohorts, periods, and covariate cells, a finite 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 finite 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 finite 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 candidate satisfying the supplied cell normal equation. On any treated cohort-time cell (g,t), the supplied POLS coefficient candidate equals the imputation residual mean at that cell.
Formal statement
Proof (Lean source)
ETWFE candidate satisfying the supplied cell normal equation. On any treated cohort-time cell (g,t), the supplied extended two-way-fixed-effects (ETWFE) coefficient candidate equals the imputation residual mean at that cell.
Formal statement
Proof (Lean source)
The weighted linear aggregate of supplied imputation coefficients for a finite cell system, untreated regression, and coefficient scaffold uses an arbitrary cohort-period coefficient function over finite cohort, period, and covariate sets.
Definition (Lean source)
The weighted linear aggregate of supplied pooled-least-squares coefficient candidates for a finite cell system, untreated regression, and coefficient scaffold uses an arbitrary cohort-period coefficient function over finite cohort, period, and covariate sets.
Definition (Lean source)
The weighted linear aggregate of supplied extended two-way-fixed-effects coefficient candidates for a finite cell system, untreated regression, and coefficient scaffold uses an arbitrary cohort-period coefficient function over finite cohort, period, and covariate sets.
Definition (Lean source)
Finite-cell normal-equation scaffold consequences. 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 coefficient candidates all equal the cell treatment-effect contrast, and consequently every treated-cell weighted linear aggregate of the three candidates equals the correspondingly weighted linear aggregate of those contrasts.
Formal statement
Proof (Lean source)
9 supporting declarations (lemmas, instances)
-
untreatedFittheorem — The additive fitted mean equals the cohort-specific outcome mean at an untreated cell and covariate value when an untreated-fit witness is combined with no anticipation and additive conditional parallel trends for a finite cell system over finite cohort, period, and covariate sets.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 Finset.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 -
recovers_target_Y0theorem — 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.hypothesesCohort :sharedType u_1Time :sharedType u_2hNA :NoAnticipation PhCPT :g :Cohortt :Timehgt :P.treatedCell g tc :CovarconclusionS.m0 g t c = P.Y0Mean g t cProof (Lean source)
theorem recovers_target_Y0 {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) : S.m0 g t c = P.Y0Mean g t c := by classical obtain ⟨αm, lamm, hm⟩ := S.additive obtain ⟨αy, lamy, hy⟩ := id hCPT -- The difference of the two additive representations. 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 hd_untreated : ∀ ⦃g : Cohort⦄ ⦃t : Time⦄, P.untreatedCell g t → ∀ c, d g t c = 0 := by intro g t hut c have h1 : S.m0 g t c = P.Y0Mean g t c := 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] simp [hd, h1] have hzero : d g t c = 0 := S.design_identifies d hd_add hd_untreated hgt c have := sub_eq_zero.mp (by simpa [hd] using hzero) exact this -
cellResidualNormalEq_eq_imputationThetatheorem — For outcome and fitted-mean arrays over cohort, period, and finite covariate sets, within-cohort covariate weights that sum to one make a coefficient satisfying the weighted residual normal equation equal the corresponding weighted 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 — For finite cohort and period sets, outcome and fitted-mean arrays, within-cohort covariate weights, a coefficient, and a selected cohort-period cell, the full normal equation against that cell's indicator is equivalent to its single-cell residual equation.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_imputation_of_normalEqtheorem — On a treated cell, the supplied POLS candidate equals the supplied imputation candidate, as an algebraic consequence of their scaffold identities.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_of_normalEq (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_of_normalEq P S hgt, E.thetaImp_eq_imputation hgt] -
etwfe_cell_eq_pols_of_normalEqtheorem — On a treated cell, the supplied ETWFE candidate equals the supplied POLS candidate, because both satisfy the scaffold's finite-cell normal equations.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_of_normalEq (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_of_normalEq P S hgt, E.thetaPOLS_eq_imputationTheta_of_normalEq P S hgt] -
imputationTheta_eq_tauCelltheorem — Under no anticipation, additive conditional parallel trends, and membership in the treated-cell predicate, the supplied imputation coefficient equals the cell treatment-effect contrast for a finite cell system, untreated regression, and coefficient scaffold over finite cohort, period, and covariate sets.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] -
flexible_did_cell_consequences_of_scaffoldtheorem — Cell-level consequences of supplied POLS and ETWFE normal equations. 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 scaffold E, which supplies the imputation identity and POLS/ETWFE cell normal equations, then the three supplied coefficient candidates at (g,t) all equal the cell treatment-effect contrast.hypothesesCohort :sharedType u_1Time :sharedType u_2Covar :sharedType u_3P :StaggeredATTCells Cohort Time CovarE :hNA :NoAnticipation PhCPT :g :Cohortt :Timehgt :P.treatedCell g tconclusionconclusion 1E.thetaImp g t = P.tauCell g tconclusion 2E.thetaPOLS g t = P.tauCell g tconclusion 3E.thetaETWFE g t = P.tauCell g tProof (Lean source)
theorem flexible_did_cell_consequences_of_scaffold (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 ∧ E.thetaPOLS g t = P.tauCell g t ∧ E.thetaETWFE g t = P.tauCell g t := by have himp : E.thetaImp g t = P.tauCell g t := imputationTheta_eq_tauCell P S E hNA hCPT hgt have hpols : E.thetaPOLS g t = P.tauCell g t := by rw [E.pols_cell_eq_imputation_of_normalEq P S hgt, himp] have hetwfe : E.thetaETWFE g t = P.tauCell g t := by rw [E.etwfe_cell_eq_pols_of_normalEq P S hgt, hpols] exact ⟨himp, hpols, hetwfe⟩ -
flexible_did_aggregate_consequences_of_scaffoldtheorem — Aggregate consequences of supplied POLS and ETWFE normal equations. 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 coefficient function a, the a-weighted linear aggregates of the three supplied coefficient candidates all equal the same linear aggregate of cell treatment-effect contrasts. No nonnegativity or normalization of a is assumed.hypothesesCohort :sharedType u_1Time :sharedType u_2Covar :sharedType u_3P :StaggeredATTCells Cohort Time CovarE :hNA :NoAnticipation PhCPT :a :Cohort → Time → ℝProof (Lean source)
theorem flexible_did_aggregate_consequences_of_scaffold (P : StaggeredATTCells Cohort Time Covar) (S : SaturatedUntreatedRegression P) (E : FlexibleDIDEstimands P S) (hNA : NoAnticipation P) (hCPT : ConditionalParallelTrendsAdditive P) (a : Cohort → Time → ℝ) : psiImp P E a = P.tauAgg a ∧ psiPOLS P E a = P.tauAgg a ∧ psiETWFE P E a = P.tauAgg a := by classical have hcell : ∀ gt ∈ P.treatedCells, E.thetaImp gt.1 gt.2 = P.tauCell gt.1 gt.2 ∧ E.thetaPOLS gt.1 gt.2 = P.tauCell gt.1 gt.2 ∧ E.thetaETWFE gt.1 gt.2 = P.tauCell gt.1 gt.2 := by intro gt hgt_mem have hgt : P.treatedCell gt.1 gt.2 := by simpa [StaggeredATTCells.treatedCells] using hgt_mem exact flexible_did_cell_consequences_of_scaffold P S E hNA hCPT hgt constructor · unfold psiImp StaggeredATTCells.tauAgg refine Finset.sum_congr rfl ?_ intro gt hgt rw [(hcell gt hgt).1] constructor · unfold psiPOLS StaggeredATTCells.tauAgg refine Finset.sum_congr rfl ?_ intro gt hgt rw [(hcell gt hgt).2.1] · unfold psiETWFE StaggeredATTCells.tauAgg refine Finset.sum_congr rfl ?_ intro gt hgt rw [(hcell gt hgt).2.2]
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 scalar TWFE coefficient solves its normal equation for a finite balanced-panel regression problem over finite unit and period sets, because its residualized regressor has positive 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 — Any coefficient satisfying the scalar TWFE normal equation equals the closed-form TWFE coefficient for a full-rank finite balanced-panel problem over finite unit and period sets.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 — Every function satisfying the scalar two-way Mundlak nuisance representation is additive in a unit component and a period component for a regressor and two families of controls over finite unit, period, and control sets.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 — For a scalar finite-panel regression problem and unit-only and period-only control families, the regressor minus its double demean is unit-time additive and the double-demeaned regressor is orthogonal to every two-way Mundlak nuisance function over finite unit, period, and control sets.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) P.X h (mundlak_nuisance_unit_time P.X Zvar Mvar hh) -
twfe_twm_optional_controls_invarianttheorem — Two scalar two-way Mundlak fits using possibly different unit-only and period-only controls have the same regressor coefficient for one finite-panel problem over finite unit, period, and control sets.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 — For a vector regressor array, an outcome array, and a candidate coefficient vector over finite unit, period, and regressor-coordinate sets, the coordinate-wise residual normal equations are equivalent to the residualized Gram-matrix normal equation.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 — For a scalar finite balanced-panel regression problem over finite unit and period sets, the sole coordinate of its vector embedding's TWFE coefficient equals the scalar TWFE coefficient.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 the population conditional mean of an integrable effect for a cell system and untreated fit at a selected cohort and period over finite cohort, period, and covariate sets. This holds in a finite-measure model for an integrable effect on a measurable cohort event when measurable, pairwise-disjoint covariate cells partition the sample space, the supplied weights are the corresponding conditional probabilities, and the finite residuals are the within-cell conditional means.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 :conclusionimputationTheta P S g t = normalizedRestrictedIntegral μ 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 = normalizedRestrictedIntegral μ (cohortEvent ∩ covarCell c) Δ) : imputationTheta P S g t = normalizedRestrictedIntegral μ 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 — Under no anticipation and additive conditional parallel trends, the fitted untreated mean equals the population conditional mean of the untreated outcome for a cell system and saturated untreated regression at a treated cell and covariate value over finite cohort, period, and covariate sets. The population quantity is supplied by a measure model, cell events and an untreated outcome, and the identification of the primitive cell mean with that conditional mean.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 = normalizedRestrictedIntegral μ (cellEvent g t c) Y0popconclusionS.m0 g t c = normalizedRestrictedIntegral μ (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 = normalizedRestrictedIntegral μ (cellEvent g t c) Y0pop) : S.m0 g t c = normalizedRestrictedIntegral μ (cellEvent g t c) Y0pop := by rw [S.recovers_target_Y0 hNA hCPT hgt c, hY0] -
m0_eq_eventCondExp_untreatedtheorem — Under no anticipation and additive conditional parallel trends, the fitted untreated mean equals the population conditional mean of the untreated outcome for a cell system and saturated untreated regression at an untreated cell and covariate value over finite cohort, period, and covariate sets. The population quantity is supplied by a measure model, cell events and an untreated outcome, and the identification of the primitive cell mean with that conditional mean.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 = normalizedRestrictedIntegral μ (cellEvent g t c) Y0popconclusionS.m0 g t c = normalizedRestrictedIntegral μ (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 = normalizedRestrictedIntegral μ (cellEvent g t c) Y0pop) : S.m0 g t c = normalizedRestrictedIntegral μ (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 only the outcome-mean component of a finite cell system from an underlying measure. ★ ofPopulation★ m0_eq_eventCondExp_treated_ofPopulation★ m0_eq_eventCondExp_untreated_ofPopulation
Wooldridge Population Origin
This file constructs only the outcome-mean component of a finite cell system
from an underlying measure. StaggeredATTCells.ofPopulation defines the three
cell means as normalized restricted integrals and derives their consistency
fields from pointwise potential-outcome consistency. Cell events, treatment
predicates, cohort shares, and covariate weights are supplied independently;
the constructor does not prove that they arise from one probability model. The
two m0_eq_eventCondExp_*_ofPopulation corollaries specialize the population
bridge, making only the untreated-outcome mean identification definitional.
The finite cell system with population-defined outcome means uses measure, events, and three outcomes over finite cohort, period, and covariate sets, while carrying supplied data unchanged. Measurable, positive-mass cells and cellwise integrability support the conditional-mean interpretation; weight conditions and pointwise consistency supply the remaining fields.
Definition (Lean source)
The probability-measure specialization of the outcome-mean constructor uses probability, events, and three outcomes over finite cohort, period, and covariate sets, while carrying supplied predicates, shares, and weights unchanged. It assumes measurable positive-probability cells, cellwise integrability, weight conditions, and pointwise factual-outcome consistency, exactly as the measure-based constructor does.
Definition (Lean source)
When a system's outcome means come from population integrals, its treated-cell untreated fit has the same origin. 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 uses the constructor's population-defined outcome means and supplied remaining data 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)
When a system's outcome means come from population integrals, its untreated-cell fit has the same origin. Fix population outcomes Y0pop, Ygpop, and Yobspop on a measured sample space; 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 uses the constructor's population-defined outcome means and supplied remaining data 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 (2025, Theorem 3.1). 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 — For a vector regressor array over finite unit and period sets and a regressor-coordinate set, the specialized residualized Gram matrix equals the generic Gram matrix applied to the double-demeaned regressors.hypothesesUnit :sharedType u_1Time :sharedType u_2K :sharedType u_3X :Unit → Time → K → ℝ -
numer_eq_numerOftheorem — For a vector regressor array and an outcome array over finite unit and period sets and a regressor-coordinate set, the specialized residualized numerator equals the generic numerator applied to the double-demeaned arrays.hypothesesUnit :sharedType u_1Time :sharedType u_2K :sharedType u_3X :Unit → Time → K → ℝY :Unit → Time → ℝ -
sum_dotRegressortheorem — For two vector regressor arrays, a coefficient vector, and a selected coordinate over finite unit, period, and coordinate sets, the summed product of that coordinate with the fitted regressor combination factors through the cross-Gram sums.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 — The candidate coefficient equals the residualized matrix coefficient over finite unit, period, and regressor-coordinate sets when the outcome and regressors split into projected and residual parts, the projected regressors and fitted nuisance belong to a specified nuisance class, the residualized regressors satisfy the required orthogonality conditions, their Gram matrix is nonsingular, and the raw residual satisfies the regressor and nuisance normal equations.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 — Every function satisfying the vector two-way Mundlak nuisance representation is additive in a unit component and a period component for a vector regressor and two control families over finite unit, period, coordinate, and control sets.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 — For a selected coordinate and a coordinate-indexed function on a finite coordinate set, summing after multiplication by the selected coordinate's zero-one indicator returns 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 — Two vector two-way Mundlak fits using possibly different unit-only and period-only controls have the same regressor coefficient vector for one vector finite-panel problem over finite index sets.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₂]