Panel.EstimandCharacterization.StaggeredTWFEDecomposition
The Goodman-Bacon decomposition: TWFE-DiD as a weighted average of 2x2 comparisons, with the weight formulas.
FinitePanel 34 core · 4 supporting This file provides the finite cohort-period primitives for the Goodman-Bacon two-way fixed-effect decomposition. ★ Dtilde_eq
Goodman-Bacon Panel Algebra
This file provides the finite cohort-period primitives for the Goodman-Bacon two-way fixed-effect decomposition. It defines staggered adoption panels, absorbing treatment, residualized treatment, the TWFE coefficient, comparison windows, pairwise comparison contrasts, and the raw and normalized weights for treated-versus-never, early-versus-late, and late-versus-early comparisons.
The three-category comparison label classifies each admissible two-by-two comparison as a treated cohort against a never-treated cohort, an early-adopting cohort against a later-adopting cohort before the latter adopts, or a later-adopting cohort against an early-adopting cohort after the latter adopts.
Definition (Lean source)
A staggered-adoption cohort panel: a cell-statistics record carrying, per cohort, a population share, an adoption date — a finite period, or ⊤ for the never-treated case, and the cohort-period factual outcome mean, subject to a positive number of periods, strictly positive cohort shares, and cohort shares summing to one.
Definition (Lean source)
For a cohort panel, a cohort, and a period, the treatment indicator equals one if the cohort has adopted by that period and zero otherwise, and is therefore binary and absorbing.
Definition (Lean source)
For a cohort panel and a cohort, the cohort treatment share is that cohort's treatment indicator averaged over all panel periods.
Definition (Lean source)
For a cohort panel, the overall treatment share is the sum of each cohort's population share times its average treatment indicator.
Definition (Lean source)
For a cohort panel, the cohort weight system assigns each cohort its population share and carries the panel's positivity and unit-sum conditions.
Definition (Lean source)
For a cohort panel, a cohort, and a period, the residualized treatment is the treatment indicator minus its cohort mean and its cross-cohort period mean, plus the grand mean.
Definition (Lean source)
For a cohort panel and a cohort-period cell, the double-demeaned residualized treatment Dtilde P g t equals the original Goodman-Bacon closed form: the raw treatment minus the cohort mean, minus the period cross-cohort mean, plus the grand mean.
Formal statement
Proof (Lean source)
For a cohort panel, the residualized-treatment variance is the sum, over cohorts and periods, of the cohort share divided by the number of periods times squared residualized treatment.
Definition (Lean source)
For a cohort panel, the finite-cell population two-way-fixed-effects coefficient is the weighted covariance of residualized treatment and factual outcomes divided by residualized-treatment variance; it is defined even when that denominator is zero.
Definition (Lean source)
For a cohort panel, a cohort, and a set of periods, the factual-outcome window mean is the average factual outcome for that cohort over the specified periods, and is defined as zero when the set is empty.
Definition (Lean source)
For a cohort panel and a cohort, the treated-versus-never untreated window is the set of all panel periods before that cohort's adoption date.
Definition (Lean source)
For a cohort panel and a cohort, the treated-versus-never treated window is the set of all panel periods at or after that cohort's adoption date.
Definition (Lean source)
For a cohort panel and an early-adopting cohort, the early-versus-late untreated window is the set of all periods before the early cohort's adoption date.
Definition (Lean source)
For a cohort panel, an early cohort, and a late cohort, the early-versus-late treated window is the set of periods from the early cohort's adoption through the period before the late cohort's adoption.
Definition (Lean source)
For a cohort panel, an early cohort, and a late cohort, the late-versus-early early-treated window is the set of periods from the early cohort's adoption through the period before the late cohort's adoption.
Definition (Lean source)
For a cohort panel and a late cohort, the late-versus-early both-treated window is the set of all periods at or after the late cohort's adoption date.
Definition (Lean source)
For a cohort panel, a treated cohort, and a never-treated comparison cohort, the treated-versus-never two-by-two difference-in-differences contrast is the treated cohort's outcome change between its treated and untreated windows minus the comparison cohort's change over those same windows.
For a cohort panel, an early cohort, and a late cohort, the early-versus-late two-by-two difference-in-differences contrast is the early cohort's outcome change from its untreated to its treated-before-late window minus the late cohort's change over those same windows.
For a cohort panel, an early cohort, and a late cohort, the late-versus-early two-by-two difference-in-differences contrast is the late cohort's outcome change from the early-treated window to the both-treated window minus the early cohort's change over those same windows.
For a cohort panel, a treated cohort, and a never-treated cohort, the treated-versus-never raw weight is the product of their population shares and the treated cohort's average treatment indicator times one minus that indicator.
Definition (Lean source)
For a cohort panel, an early cohort, and a late cohort, the treatment-share gap is the early cohort's average treatment indicator minus the late cohort's average treatment indicator.
Definition (Lean source)
For a cohort panel, an early cohort, and a late cohort, the comparison splitting fraction is one minus the early cohort's treatment share divided by one minus their treatment-share gap, with the usual zero-denominator convention.
Definition (Lean source)
For a cohort panel, an early cohort, and a late cohort, the early-versus-late raw weight is the product of their shares, their treatment-share gap, one minus that gap, and the comparison splitting fraction.
Definition (Lean source)
For a cohort panel, an early cohort, and a late cohort, the late-versus-early raw weight is the product of their shares, their treatment-share gap, one minus that gap, and one minus the comparison splitting fraction.
Definition (Lean source)
For a cohort panel, the aggregate raw-weight denominator is the sum of treated-versus-never raw weights for finite-versus-never-treated pairs and the two timing-comparison raw weights for ordered finite adoption-date pairs.
Definition (Lean source)
For a cohort panel, a treated cohort, and a never-treated cohort, the normalized treated-versus-never weight is its raw weight divided by the aggregate raw-weight denominator.
Definition (Lean source)
For a cohort panel, an early cohort, and a late cohort, the normalized early-versus-late weight is its raw weight divided by the aggregate raw-weight denominator.
Definition (Lean source)
For a cohort panel, an early cohort, and a late cohort, the normalized late-versus-early weight is its raw weight divided by the aggregate raw-weight denominator.
Definition (Lean source)
For a cohort panel and a tagged ordered cohort pair, the admissibility condition holds precisely when a treated-versus-never tag pairs an eventually treated cohort with a never-treated cohort, or either timing-comparison tag orders two finitely adopting cohorts by adoption date, and in every case both cohort shares are positive.
Definition (Lean source)
For a cohort panel, the comparison index set is the finite set of every tagged ordered cohort pair satisfying the admissibility condition.
Definition (Lean source)
For a cohort panel and a tagged ordered cohort pair, the unified normalized weight is the normalized weight associated with that pair's comparison tag when the pair is admissible, and zero otherwise.
Definition (Lean source)
For a cohort panel and a tagged ordered cohort pair, the unified two-by-two contrast is the contrast associated with that pair's comparison tag when the pair is admissible, and zero otherwise.
Definition (Lean source)
For a cohort panel and a tagged ordered cohort pair, the unified raw weight is the raw weight associated with that pair's comparison tag when the pair is admissible, and zero otherwise.
Definition (Lean source)
4 supporting declarations (lemmas, instances)
-
instDecidableEqCompTaginductiveinductiveconstructorsTN :EL :LE :deriving DecidableEq -
instFintypeCompTaginstance — A finite enumeration of the three comparison labels consists exactly of the treated-versus-never, early-versus-late, and late-versus-early categories. -
barD_eq_unitMeantheorem — Goodman-Bacon's cohort treatment share is the shared unit mean.hypothesesconclusionbarD P g = WeightedTwoWayPanel.unitMean (D P) gProof (Lean source)
theorem barD_eq_unitMean (P : CohortPanel 𝒢 T) (g : 𝒢) : barD P g = WeightedTwoWayPanel.unitMean (D P) g := by simp [barD, WeightedTwoWayPanel.unitMean] -
pCohort_eq_grandMeantheorem — Goodman-Bacon's overall treatment share is the shared weighted grand mean.hypothesesconclusionpCohort P = WeightedTwoWayPanel.grandMean (cohortWeights P) (D P)Proof (Lean source)
theorem pCohort_eq_grandMean (P : CohortPanel 𝒢 T) : pCohort P = WeightedTwoWayPanel.grandMean (cohortWeights P) (D P) := by simp [pCohort, WeightedTwoWayPanel.grandMean, cohortWeights, ← barD_eq_unitMean]
Causal 6 core · 9 supporting This file gives the causal layer of the Goodman-Bacon staggered-timing decomposition. ★ Δ_TN_eq_ATT★ Δ_EL_eq_ATT★ Δ_LE_eq_bad_comparison
Goodman-Bacon Causal Characterization
This file gives the causal layer of the Goodman-Bacon staggered-timing decomposition. Under two-state potential-outcome assumptions, consistency, no anticipation, and pairwise untreated parallel trends, it identifies the treated-versus-never and early-versus-late contrasts with window-specific average treatment effects and expresses the late-versus-early contrast with its bad-comparison adjustment.
The never-treated mean outcome over a period window averages a cohort's never-treated potential outcomes across the selected periods and is zero for an empty window.
The window-specific average treatment effect on the treated averages the difference between own-adoption potential outcomes and never-treated potential outcomes for a cohort across the selected periods, and is zero for an empty window.
The causal model for a cohort panel, never-treated potential outcomes, and own-adoption potential outcomes combines consistency after adoption, consistency with never treatment before adoption, no anticipation across the two potential-outcome paths, and untreated parallel trends for treated-versus-never comparisons, early-versus-late comparisons, and late-versus-early comparisons.
Definition (Lean source)
Consistency on treated cells: when A_g ≤ t, the factual outcome
equals the post-adoption potential outcome.
Consistency on untreated cells: when t < A_g, the factual outcome
equals the never-treated potential outcome.
No anticipation: pre-adoption potential outcomes coincide.
Pairwise untreated parallel trends for treated-vs-never (TN).
Pairwise untreated parallel trends for early-vs-late before late (EL).
Under the packaged causal assumptions linking a cohort panel to never-treated and own-adoption potential-outcome paths, the DID comparison of a treated and a never-treated cohort identifies the treated cohort's post-adoption window effect when their adoption dates are respectively finite and infinite, and the treated cohort has a pre-treatment period.
Formal statement
Proof (Lean source)
Under the packaged causal assumptions linking a cohort panel to never-treated and own-adoption potential-outcome paths, the DID comparison of an early and a late cohort identifies the early cohort's effect over the between-adoption window when the early cohort adopts first, the late cohort eventually adopts, and the early cohort has a pre-treatment period.
Formal statement
Proof (Lean source)
Layer C corollary 3 — LE has a bad-comparison term. Fix a cohort panel P and potential-outcome maps Y0, Y1, and assume consistency on treated and untreated cells, no anticipation, and pairwise untreated parallel trends across the three comparison types. For an early cohort e whose adoption date strictly precedes that of a late cohort ℓ, with ℓ's adoption date finite, the late-versus-early contrast Δ_LE equals ℓ's window-specific average treatment effect on the treated over its post-adoption window, minus the "bad-comparison" gap between e's own treatment effects on the two comparison windows:
Formal statement
Proof (Lean source)
9 supporting declarations (lemmas, instances)
-
Ybar_eq_Ybar0_on_S0_TNtheorem — On the untreated window S0_TN P g = {t : t < A_g}, the factual Ybar of cohort g equals the never-treated Ybar0: by consistencyUntreated on each cell.hypotheses𝒢 :sharedType u_1hConsistency :∀ g tifAdoptionPath.lt (P.A g) tthenP.Y g t = Y0 g tg :𝒢Proof (Lean source)
theorem Ybar_eq_Ybar0_on_S0_TN (hConsistency : ∀ g t, AdoptionPath.lt (P.A g) t → P.Y g t = Y0 g t) (g : 𝒢) : Ybar P g (S0_TN P g) = Ybar0 Y0 g (S0_TN P g) := by classical unfold Ybar Ybar0 congr 1 refine Finset.sum_congr rfl ?_ intro t ht have htlt : AdoptionPath.lt (P.A g) t := by simpa only [S0_TN, mem_filter, Finset.mem_univ, true_and, Set.mem_ofPred_eq] using ht exact hConsistency g t htlt -
Ybar_eq_Ybar0_of_inftheorem — On any window S where every period is untreated for cohort u, the factual Ybar equals the never-treated Ybar0.hypotheses𝒢 :sharedType u_1hConsistency :∀ g tifAdoptionPath.lt (P.A g) tthenP.Y g t = Y0 g tu :𝒢hS :∀ t ∈ S, AdoptionPath.lt (P.A u) tProof (Lean source)
theorem Ybar_eq_Ybar0_of_inf (hConsistency : ∀ g t, AdoptionPath.lt (P.A g) t → P.Y g t = Y0 g t) {u : 𝒢} (S : Finset (Fin T)) (hS : ∀ t ∈ S, AdoptionPath.lt (P.A u) t) : Ybar P u S = Ybar0 Y0 u S := by classical unfold Ybar Ybar0 congr 1 refine Finset.sum_congr rfl ?_ intro t ht exact hConsistency u t (hS t ht) -
Ybar_eq_Ybar0_add_ATT_of_treatedtheorem — On a window where every cell is treated for cohort g, the factual Ybar decomposes as the never-treated mean plus the window ATT.hypotheses𝒢 :sharedType u_1hConsistency :∀ g tifAdoptionPath.le (P.A g) tthenP.Y g t = Y1 g tg :𝒢hS :∀ t ∈ S, AdoptionPath.le (P.A g) tconclusionProof (Lean source)
theorem Ybar_eq_Ybar0_add_ATT_of_treated (hConsistency : ∀ g t, AdoptionPath.le (P.A g) t → P.Y g t = Y1 g t) (g : 𝒢) (S : Finset (Fin T)) (hS : ∀ t ∈ S, AdoptionPath.le (P.A g) t) : Ybar P g S = Ybar0 Y0 g S + ATT_window Y0 Y1 g S := by classical unfold Ybar Ybar0 ATT_window rw [← mul_add] congr 1 calc ∑ t ∈ S, P.Y g t = ∑ t ∈ S, Y1 g t := by refine Finset.sum_congr rfl ?_ intro t ht exact hConsistency g t (hS t ht) _ = ∑ t ∈ S, (Y0 g t + (Y1 g t - Y0 g t)) := by refine Finset.sum_congr rfl ?_ intro t _ ring _ = ∑ t ∈ S, Y0 g t + ∑ t ∈ S, (Y1 g t - Y0 g t) := by exact Finset.sum_add_distrib -
Ybar_eq_Ybar0_on_S0_ELtheorem — On the early-cohort untreated window S0_EL P e = {t : t < A_e}, the factual Ybar of cohort e equals the never-treated Ybar0.hypotheses𝒢 :sharedType u_1hConsistency :∀ g tifAdoptionPath.lt (P.A g) tthenP.Y g t = Y0 g te :𝒢Proof (Lean source)
theorem Ybar_eq_Ybar0_on_S0_EL (hConsistency : ∀ g t, AdoptionPath.lt (P.A g) t → P.Y g t = Y0 g t) (e : 𝒢) : Ybar P e (S0_EL P e) = Ybar0 Y0 e (S0_EL P e) := by classical unfold Ybar Ybar0 congr 1 refine Finset.sum_congr rfl ?_ intro t ht have htlt : AdoptionPath.lt (P.A e) t := by simpa only [S0_EL, mem_filter, Finset.mem_univ, true_and, Set.mem_ofPred_eq] using ht exact hConsistency e t htlt -
Ybar_eq_Ybar0_late_on_S1_ELtheorem — The late-cohort factual Ybar on S1_EL P e ℓ = {A_e ≤ t < A_ℓ} equals the never-treated Ybar0: each cell satisfies t < A_ℓ.hypotheses𝒢 :sharedType u_1hConsistency :∀ g tifAdoptionPath.lt (P.A g) tthenP.Y g t = Y0 g te ℓ :𝒢Proof (Lean source)
theorem Ybar_eq_Ybar0_late_on_S1_EL (hConsistency : ∀ g t, AdoptionPath.lt (P.A g) t → P.Y g t = Y0 g t) (e ℓ : 𝒢) : Ybar P ℓ (S1_EL P e ℓ) = Ybar0 Y0 ℓ (S1_EL P e ℓ) := by classical unfold Ybar Ybar0 congr 1 refine Finset.sum_congr rfl ?_ intro t ht have htmem : AdoptionPath.le (P.A e) t ∧ AdoptionPath.lt (P.A ℓ) t := by simpa only [S1_EL, mem_filter, Finset.mem_univ, true_and, Set.mem_ofPred_eq] using ht exact hConsistency ℓ t htmem.2 -
Ybar_eq_Ybar0_late_on_S0_ELtheorem — The late-cohort factual Ybar on S0_EL P e = {t : t < A_e} equals the never-treated Ybar0 when A_e < A_ℓ.hypotheses𝒢 :sharedType u_1hConsistency :∀ g tifAdoptionPath.lt (P.A g) tthenP.Y g t = Y0 g te ℓ :𝒢h_lt :P.A e < P.A ℓProof (Lean source)
theorem Ybar_eq_Ybar0_late_on_S0_EL (hConsistency : ∀ g t, AdoptionPath.lt (P.A g) t → P.Y g t = Y0 g t) (e ℓ : 𝒢) (h_lt : P.A e < P.A ℓ) : Ybar P ℓ (S0_EL P e) = Ybar0 Y0 ℓ (S0_EL P e) := by classical unfold Ybar Ybar0 congr 1 refine Finset.sum_congr rfl ?_ intro t ht have htlt : (t : WithTop (Fin T)) < P.A e := by have h0 : AdoptionPath.lt (P.A e) t := by simpa only [S0_EL, mem_filter, Finset.mem_univ, true_and, Set.mem_ofPred_eq] using ht exact h0 exact hConsistency ℓ t (by simpa [AdoptionPath.lt] using lt_trans htlt h_lt) -
Ybar_eq_Ybar0_late_on_S0_LEtheorem — The late-cohort factual Ybar on S0_LE P e ℓ = {A_e ≤ t < A_ℓ} equals the never-treated Ybar0.hypotheses𝒢 :sharedType u_1hConsistency :∀ g tifAdoptionPath.lt (P.A g) tthenP.Y g t = Y0 g te ℓ :𝒢Proof (Lean source)
theorem Ybar_eq_Ybar0_late_on_S0_LE (hConsistency : ∀ g t, AdoptionPath.lt (P.A g) t → P.Y g t = Y0 g t) (e ℓ : 𝒢) : Ybar P ℓ (S0_LE P e ℓ) = Ybar0 Y0 ℓ (S0_LE P e ℓ) := by classical unfold Ybar Ybar0 congr 1 refine Finset.sum_congr rfl ?_ intro t ht have htmem : AdoptionPath.le (P.A e) t ∧ AdoptionPath.lt (P.A ℓ) t := by simpa only [S0_LE, S1_EL, mem_filter, Finset.mem_univ, true_and, Set.mem_ofPred_eq] using ht exact hConsistency ℓ t htmem.2 -
Δ_TN_eq_ATT_totalizedtheorem — Under the packaged causal assumptions linking a cohort panel to never-treated and own-adoption potential-outcome paths, the totalized comparison of a treated and a never-treated cohort equals the treated cohort's totalized post-adoption window effect when their adoption dates are respectively finite and infinite.hypotheses𝒢 :sharedType u_1T :sharedℕP :CohortPanel 𝒢 TY0 Y1 :𝒢 → Fin T → ℝhA :CausalAssumptions P Y0 Y1g u :𝒢h_g_fin :AdoptionPath.isFinite (P.A g)h_u_inf :AdoptionPath.isInfinite (P.A u)conclusionProof (Lean source)
theorem Δ_TN_eq_ATT_totalized (P : CohortPanel 𝒢 T) (Y0 Y1 : 𝒢 → Fin T → ℝ) (hA : CausalAssumptions P Y0 Y1) (g u : 𝒢) (h_g_fin : AdoptionPath.isFinite (P.A g)) (h_u_inf : AdoptionPath.isInfinite (P.A u)) : Δ_TN P g u = ATT_window Y0 Y1 g (S1_TN P g) := by classical have h_treated : Ybar P g (S1_TN P g) = Ybar0 Y0 g (S1_TN P g) + ATT_window Y0 Y1 g (S1_TN P g) := by exact CausalAssumptions.Ybar_eq_Ybar0_add_ATT_of_treated hA.consistencyTreated g (S1_TN P g) (by intro t ht simpa only [S1_TN, mem_filter, Finset.mem_univ, true_and, Set.mem_ofPred_eq] using ht) have h_g0 := CausalAssumptions.Ybar_eq_Ybar0_on_S0_TN hA.consistencyUntreated g have h_u1 := CausalAssumptions.Ybar_eq_Ybar0_of_inf hA.consistencyUntreated (S1_TN P g) (fun _ _ => AdoptionPath.lt_of_isInfinite h_u_inf) have h_u0 := CausalAssumptions.Ybar_eq_Ybar0_of_inf hA.consistencyUntreated (S0_TN P g) (fun _ _ => AdoptionPath.lt_of_isInfinite h_u_inf) have hPT := hA.parallelTrends_TN g u h_g_fin h_u_inf unfold Δ_TN rw [h_treated, h_g0, h_u1, h_u0] linarith -
Δ_EL_eq_ATT_totalizedtheorem — Under the packaged causal assumptions linking a cohort panel to never-treated and own-adoption potential-outcome paths, the totalized comparison of an early and a late cohort equals the early cohort's totalized effect over the between-adoption window when the early cohort adopts first and the late cohort eventually adopts.hypotheses𝒢 :sharedType u_1T :sharedℕP :CohortPanel 𝒢 TY0 Y1 :𝒢 → Fin T → ℝhA :CausalAssumptions P Y0 Y1e ℓ :𝒢h_lt :P.A e < P.A ℓh_ℓ_fin :AdoptionPath.isFinite (P.A ℓ)conclusionProof (Lean source)
theorem Δ_EL_eq_ATT_totalized (P : CohortPanel 𝒢 T) (Y0 Y1 : 𝒢 → Fin T → ℝ) (hA : CausalAssumptions P Y0 Y1) (e ℓ : 𝒢) (h_lt : P.A e < P.A ℓ) (h_ℓ_fin : AdoptionPath.isFinite (P.A ℓ)) : Δ_EL P e ℓ = ATT_window Y0 Y1 e (S1_EL P e ℓ) := by classical have h_e1 : Ybar P e (S1_EL P e ℓ) = Ybar0 Y0 e (S1_EL P e ℓ) + ATT_window Y0 Y1 e (S1_EL P e ℓ) := by exact CausalAssumptions.Ybar_eq_Ybar0_add_ATT_of_treated hA.consistencyTreated e (S1_EL P e ℓ) (by intro t ht have htmem : AdoptionPath.le (P.A e) t ∧ AdoptionPath.lt (P.A ℓ) t := by simpa only [S1_EL, mem_filter, Finset.mem_univ, true_and, Set.mem_ofPred_eq] using ht exact htmem.1) have h_e0 := CausalAssumptions.Ybar_eq_Ybar0_on_S0_EL hA.consistencyUntreated e have h_l1 := CausalAssumptions.Ybar_eq_Ybar0_late_on_S1_EL hA.consistencyUntreated e ℓ have h_l0 := CausalAssumptions.Ybar_eq_Ybar0_late_on_S0_EL hA.consistencyUntreated e ℓ h_lt have hPT := hA.parallelTrends_EL e ℓ h_lt h_ℓ_fin unfold Δ_EL rw [h_e1, h_e0, h_l1, h_l0] linarith
AlgebraicDecomposition 3 core · 11 supporting This file establishes the finite staggered-adoption Goodman-Bacon algebraic decomposition of a two-way fixed effects coefficient into admissible two-group comparisons. ★ weights_nonneg★ weights_sum_one★ twfe_eq_weighted_avg
Goodman-Bacon Decomposition
This file establishes the finite staggered-adoption Goodman-Bacon algebraic decomposition of a two-way fixed effects coefficient into admissible two-group comparisons. It proves nonnegativity of the raw comparison weights, the denominator and numerator identities, normalization of the weights under positive residualized-treatment variance, and the corresponding weighted-average identity.
Prop A5.1 (weights_nonneg). For a cohort panel and any comparison-type index, the raw Goodman-Bacon comparison weight is nonnegative.
Formal statement
Proof (Lean source)
Prop A5.4 (weights_sum_one). For a finite Goodman–Bacon cohort panel P, if the residualized-treatment variance VD P is strictly positive, then the normalized comparison weights sum to one over all admissible 2×2 comparisons: Σ_{k ∈ 𝒦 P} weight P k = 1.
Formal statement
Proof (Lean source)
Theorem A5.5 (twfe_eq_weighted_avg, thm:po-estimand-goodman-bacon-decomposition). For a cohort panel whose residualized-treatment variance is strictly positive, the two-way fixed-effects (TWFE) coefficient equals a weighted average of admissible two-by-two DID contrasts across comparison groups. The positivity condition makes the normalized weights sum to one by weights_sum_one.
Formal statement
Proof (Lean source)
11 supporting declarations (lemmas, instances)
-
barD_eq_zero_of_isInflemma — A never-treated cohort has zero average treatment over the panel.hypothesesconclusionbarD P g = 0Proof (Lean source)
lemma barD_eq_zero_of_isInf (P : CohortPanel 𝒢 T) {g : 𝒢} (hg : AdoptionPath.isInfinite (P.A g)) : barD P g = 0 := by unfold barD simp [D_eq_zero_of_isInf P hg] -
lambdaTN_eq_gap_of_isInflemma — When one cohort is never treated, its raw comparison weight with another cohort equals the product of their cohort shares, the gap in their average treatment rates, and one minus that gap.hypothesesconclusionlambdaTN P g u = P.p g * P.p u * q P g u * (1 - q P g u)Proof (Lean source)
lemma lambdaTN_eq_gap_of_isInf (P : CohortPanel 𝒢 T) {g u : 𝒢} (hu : AdoptionPath.isInfinite (P.A u)) : lambdaTN P g u = P.p g * P.p u * q P g u * (1 - q P g u) := by unfold lambdaTN q rw [barD_eq_zero_of_isInf P hu] ring -
lambdaEL_add_lambdaLE_eq_gaplemma — The two ordered raw comparison weights between two cohorts sum to the product of their cohort shares, the gap in their average treatment rates, and one minus that gap.hypothesesProof (Lean source)
lemma lambdaEL_add_lambdaLE_eq_gap (P : CohortPanel 𝒢 T) (e ℓ : 𝒢) : lambdaEL P e ℓ + lambdaLE P e ℓ = P.p e * P.p ℓ * q P e ℓ * (1 - q P e ℓ) := by unfold lambdaEL lambdaLE ring -
Lambda_eq_gap_sumslemma — The raw denominator of the staggered-adoption two-way fixed-effects decomposition equals the sum of treated-versus-never comparison terms and ordered early-versus-late comparison terms.hypothesesconclusionLambda P= (∑ g, ∑ u, if AdoptionPath.isFinite (P.A g) ∧ AdoptionPath.isInfinite (P.A u) then P.p g * P.p u * q P g u * (1 - q P g u) else 0)+ (∑ e, ∑ ℓ, if P.A e < P.A ℓ ∧ AdoptionPath.isFinite (P.A ℓ) then P.p e * P.p ℓ * q P e ℓ * (1 - q P e ℓ) else 0)Proof (Lean source)
lemma Lambda_eq_gap_sums (P : CohortPanel 𝒢 T) : Lambda P = (∑ g, ∑ u, if AdoptionPath.isFinite (P.A g) ∧ AdoptionPath.isInfinite (P.A u) then P.p g * P.p u * q P g u * (1 - q P g u) else 0) + (∑ e, ∑ ℓ, if P.A e < P.A ℓ ∧ AdoptionPath.isFinite (P.A ℓ) then P.p e * P.p ℓ * q P e ℓ * (1 - q P e ℓ) else 0) := by unfold Lambda congr 1 · refine Finset.sum_congr rfl ?_ intro g _hg refine Finset.sum_congr rfl ?_ intro u _hu by_cases h : P.A g ≠ ⊤ ∧ P.A u = ⊤ · simp [AdoptionPath.isFinite, AdoptionPath.isInfinite, h, lambdaTN_eq_gap_of_isInf P h.2] · simp [AdoptionPath.isFinite, AdoptionPath.isInfinite, h] · refine Finset.sum_congr rfl ?_ intro e _he refine Finset.sum_congr rfl ?_ intro ℓ _hℓ by_cases h : P.A e < P.A ℓ ∧ P.A ℓ ≠ ⊤ · simp [AdoptionPath.isFinite, h, lambdaEL_add_lambdaLE_eq_gap P e ℓ] · simp [AdoptionPath.isFinite, h] -
D_eq_of_A_eqlemma — Cohorts that share the same adoption date have identical treatment status in every time period.hypothesesconclusionD P g t = D P u tProof (Lean source)
lemma D_eq_of_A_eq (P : CohortPanel 𝒢 T) {g u : 𝒢} (hA : P.A g = P.A u) (t : Fin T) : D P g t = D P u t := by unfold D rw [hA] -
adoption_pair_sum_decomplemma — When a pairwise cohort contribution is zero for cohorts sharing an adoption date, its total over all cohort pairs decomposes into the four possible ordered timing comparisons.hypotheses𝒢 :sharedType u_1T :sharedℕP :CohortPanel 𝒢 Tf :𝒢 → 𝒢 → ℝhzero :∀ g uifP.A g = P.A uthenf g u = 0conclusion(∑ g, ∑ u, f g u)= (∑ g, ∑ u, if AdoptionPath.isFinite (P.A g) ∧ AdoptionPath.isInfinite (P.A u) then f g u else 0)+ (∑ g, ∑ u, if AdoptionPath.isFinite (P.A u) ∧ AdoptionPath.isInfinite (P.A g) then f g u else 0)+ (∑ g, ∑ u, if P.A g < P.A u ∧ AdoptionPath.isFinite (P.A u) then f g u else 0)+ (∑ g, ∑ u, if P.A u < P.A g ∧ AdoptionPath.isFinite (P.A g) then f g u else 0)Proof (Lean source)
lemma adoption_pair_sum_decomp (P : CohortPanel 𝒢 T) (f : 𝒢 → 𝒢 → ℝ) (hzero : ∀ g u, P.A g = P.A u → f g u = 0) : (∑ g, ∑ u, f g u) = (∑ g, ∑ u, if AdoptionPath.isFinite (P.A g) ∧ AdoptionPath.isInfinite (P.A u) then f g u else 0) + (∑ g, ∑ u, if AdoptionPath.isFinite (P.A u) ∧ AdoptionPath.isInfinite (P.A g) then f g u else 0) + (∑ g, ∑ u, if P.A g < P.A u ∧ AdoptionPath.isFinite (P.A u) then f g u else 0) + (∑ g, ∑ u, if P.A u < P.A g ∧ AdoptionPath.isFinite (P.A g) then f g u else 0) := by calc (∑ g, ∑ u, f g u) = ∑ g, ∑ u, ((if AdoptionPath.isFinite (P.A g) ∧ AdoptionPath.isInfinite (P.A u) then f g u else 0) + (if AdoptionPath.isFinite (P.A u) ∧ AdoptionPath.isInfinite (P.A g) then f g u else 0) + (if P.A g < P.A u ∧ AdoptionPath.isFinite (P.A u) then f g u else 0) + (if P.A u < P.A g ∧ AdoptionPath.isFinite (P.A g) then f g u else 0)) := by refine Finset.sum_congr rfl ?_ intro g _hg refine Finset.sum_congr rfl ?_ intro u _hu exact adoption_pair_pointwise P f hzero g u _ = _ := by simp [Finset.sum_add_distrib, add_assoc] -
gap_sums_eq_VDlemma — The total of cohort-share products times each pair's treatment-rate gap and one minus that gap, over treated-versus-never and ordered early-versus-later pairs, equals the residualized treatment variance.hypothesesconclusion(∑ g, ∑ u, if AdoptionPath.isFinite (P.A g) ∧ AdoptionPath.isInfinite (P.A u) then P.p g * P.p u * q P g u * (1 - q P g u) else 0)+ (∑ e, ∑ ℓ, if P.A e < P.A ℓ ∧ AdoptionPath.isFinite (P.A ℓ) then P.p e * P.p ℓ * q P e ℓ * (1 - q P e ℓ) else 0)= VD PProof (Lean source)
lemma gap_sums_eq_VD (P : CohortPanel 𝒢 T) : (∑ g, ∑ u, if AdoptionPath.isFinite (P.A g) ∧ AdoptionPath.isInfinite (P.A u) then P.p g * P.p u * q P g u * (1 - q P g u) else 0) + (∑ e, ∑ ℓ, if P.A e < P.A ℓ ∧ AdoptionPath.isFinite (P.A ℓ) then P.p e * P.p ℓ * q P e ℓ * (1 - q P e ℓ) else 0) = VD P := by -- Remaining denominator algebra: expand `VD`, use `P.p_sum_one`, and group -- the pairwise variance of monotone adoption indicators by adoption-date -- order. This is the finite-sum manipulation described in the NL A5.2 doc. rw [VD_eq_pairwise_centeredD P] rw [adoption_pair_sum_grouped P (vdPairContribution P) (fun g u hA => vdPairContribution_eq_zero_of_A_eq P hA)] congr 1 · refine Finset.sum_congr rfl ?_ intro g _hg refine Finset.sum_congr rfl ?_ intro u _hu by_cases h : P.A g ≠ ⊤ ∧ P.A u = ⊤ · simp [AdoptionPath.isFinite, AdoptionPath.isInfinite, h, TN_pair_vd_contribution_eq_gap P h.2] · simp [AdoptionPath.isFinite, AdoptionPath.isInfinite, h] · refine Finset.sum_congr rfl ?_ intro e _he refine Finset.sum_congr rfl ?_ intro ℓ _hℓ by_cases h : P.A e < P.A ℓ ∧ P.A ℓ ≠ ⊤ · simp [AdoptionPath.isFinite, h, TT_pair_vd_contribution_eq_gap P h.1] · simp [AdoptionPath.isFinite, h] -
raw_weight_sum_eq_VDtheorem — Prop A5.2 (raw_weight_sum_eq_VD). The aggregate raw-weight denominator equals the residualized treatment variance: Λ P = V_D P. Key denominator identity in thm:po-estimand-goodman-bacon-decomposition.Proof (Lean source)
theorem raw_weight_sum_eq_VD (P : CohortPanel 𝒢 T) : Lambda P = VD P := by rw [Lambda_eq_gap_sums] exact gap_sums_eq_VD P -
twfe_numerator_eq_lambda_delta_sumtheorem — Prop A5.3 (twfe_numerator_eq_lambda_delta_sum). The TWFE numerator decomposes by unordered cohort pairs into raw-weight times 2x2 DID contrast contributions.hypothesesProof (Lean source)
theorem twfe_numerator_eq_lambda_delta_sum (P : CohortPanel 𝒢 T) : (∑ g, ∑ t, (P.p g / (T : ℝ)) * Dtilde P g t * P.Y g t) = (∑ g, ∑ u, if AdoptionPath.isFinite (P.A g) ∧ AdoptionPath.isInfinite (P.A u) then lambdaTN P g u * Δ_TN P g u else 0) + (∑ e, ∑ ℓ, if P.A e < P.A ℓ ∧ AdoptionPath.isFinite (P.A ℓ) then lambdaEL P e ℓ * Δ_EL P e ℓ + lambdaLE P e ℓ * Δ_LE P e ℓ else 0) := by rw [twfe_numerator_eq_pairwise_centeredD_Y P] rw [adoption_pair_sum_grouped P (numPairContribution P) (fun g u hA => numPairContribution_eq_zero_of_A_eq P hA)] congr 1 · refine Finset.sum_congr rfl ?_ intro g _hg refine Finset.sum_congr rfl ?_ intro u _hu by_cases h : P.A g ≠ ⊤ ∧ P.A u = ⊤ · simp [AdoptionPath.isFinite, AdoptionPath.isInfinite, h, TN_pair_contribution_eq_lambda_delta P h.1 h.2] · simp [AdoptionPath.isFinite, AdoptionPath.isInfinite, h] · refine Finset.sum_congr rfl ?_ intro e _he refine Finset.sum_congr rfl ?_ intro ℓ _hℓ by_cases h : P.A e < P.A ℓ ∧ P.A ℓ ≠ ⊤ · simp [AdoptionPath.isFinite, h, TT_pair_contribution_eq_lambda_delta_sum P h.1 h.2] · simp [AdoptionPath.isFinite, h] -
sum_lambdaWeight_eq_Lambdalemma — Across all admissible comparison types and cohort pairs, the raw comparison weights sum to the aggregate normalizing denominator.hypothesesconclusion∑ k ∈ 𝒦 P, lambdaWeight P k = Lambda PProof (Lean source)
lemma sum_lambdaWeight_eq_Lambda (P : CohortPanel 𝒢 T) : ∑ k ∈ 𝒦 P, lambdaWeight P k = Lambda P := by classical rw [show (∑ k ∈ 𝒦 P, lambdaWeight P k) = ∑ k, if admissible P k then lambdaWeight P k else 0 by simp [𝒦, Finset.sum_filter]] rw [Fintype.sum_prod_type] rw [sum_compTag] simp only [lambdaWeight, admissible, P.p_pos, true_and] simp_rw [if_dup] simp_rw [Fintype.sum_prod_type] simp only [and_true] have hELLE : (∑ e, ∑ ℓ, if P.A e < P.A ℓ ∧ AdoptionPath.isFinite (P.A ℓ) then lambdaEL P e ℓ else 0) + (∑ e, ∑ ℓ, if P.A e < P.A ℓ ∧ AdoptionPath.isFinite (P.A ℓ) then lambdaLE P e ℓ else 0) = ∑ e, ∑ ℓ, if P.A e < P.A ℓ ∧ AdoptionPath.isFinite (P.A ℓ) then lambdaEL P e ℓ + lambdaLE P e ℓ else 0 := by rw [← Finset.sum_add_distrib] refine Finset.sum_congr rfl ?_ intro e he rw [← Finset.sum_add_distrib] refine Finset.sum_congr rfl ?_ intro ℓ hℓ by_cases h : P.A e < P.A ℓ ∧ P.A ℓ ≠ ⊤ <;> simp [AdoptionPath.isFinite, h] unfold Lambda rw [← hELLE] rw [add_assoc] -
twfe_eq_normalized_comparison_sumtheorem — For a cohort panel, the totalized TWFE ratio equals the totalized normalized sum of admissible two-by-two DID contrasts, including in zero-variance cases.hypothesesconclusionbetaTWFE P = ∑ k ∈ 𝒦 P, weight P k * contrast P kProof (Lean source)
theorem twfe_eq_normalized_comparison_sum (P : CohortPanel 𝒢 T) : betaTWFE P = ∑ k ∈ 𝒦 P, weight P k * contrast P k := by classical have hnum := twfe_numerator_eq_lambda_delta_sum P have hsum : ∑ k ∈ 𝒦 P, lambdaWeight P k * contrast P k = (∑ g, ∑ u, if AdoptionPath.isFinite (P.A g) ∧ AdoptionPath.isInfinite (P.A u) then lambdaTN P g u * Δ_TN P g u else 0) + (∑ e, ∑ ℓ, if P.A e < P.A ℓ ∧ AdoptionPath.isFinite (P.A ℓ) then lambdaEL P e ℓ * Δ_EL P e ℓ + lambdaLE P e ℓ * Δ_LE P e ℓ else 0) := sum_lambdaWeight_mul_contrast_eq P have hweighted : ∑ k ∈ 𝒦 P, weight P k * contrast P k = (∑ k ∈ 𝒦 P, lambdaWeight P k * contrast P k) / Lambda P := by rw [Finset.sum_div] refine Finset.sum_congr rfl ?_ intro k hk have hk' : admissible P k := by simpa [𝒦] using hk rcases k with ⟨tag, pair⟩ rcases pair with ⟨g, u⟩ cases tag <;> simp [weight, lambdaWeight, w_TN, w_EL, w_LE, hk', div_eq_mul_inv, mul_left_comm, mul_comm] calc betaTWFE P = ((∑ k ∈ 𝒦 P, lambdaWeight P k * contrast P k) / Lambda P) := by unfold betaTWFE rw [hnum] rw [← hsum] rw [← raw_weight_sum_eq_VD P] _ = ∑ k ∈ 𝒦 P, weight P k * contrast P k := by rw [hweighted]
CausalDecomposition 2 core · 1 supporting This file composes the algebraic TWFE totalized weighted-sum identity with the causal window-effect equalities, expressing the two-way fixed-effect coefficient as a sum of normalized comparison weights times potential-ou ★ twfe_po_decomposition
Goodman-Bacon fused causal decomposition
This file composes the algebraic TWFE totalized weighted-sum identity with the
causal window-effect equalities, expressing the two-way fixed-effect coefficient
as a sum of normalized comparison weights times potential-outcome window
contrasts, with the late-versus-early bad-comparison term made explicit. TN and
EL entries with empty pre-treatment windows are zero-weight bookkeeping terms,
not standalone DID identification results. A weighted-average interpretation
requires the separate positive-variance condition used by weights_sum_one.
For a finite collection of cohorts whose members can be compared for equality, a natural-number panel length, a cohort panel, two potential-outcome paths, respectively under no treatment and under treatment at the cohort's own adoption date, and a labelled ordered pair of cohorts, the causal two-by-two contrast is zero when that comparison is inadmissible; otherwise, it is the relevant window average treatment effect for a treated-versus-never-treated or early-versus-late comparison, and for a late-versus-early comparison it is the late cohort's window average treatment effect minus the early cohort's corresponding treated-period effect net of its pre-period effect.
Definition (Lean source)
Fused causal Goodman-Bacon decomposition. Fix a cohort panel P and potential-outcome maps Y0 (never-treated path) and Y1 (own-adoption-date path). Assume consistency on treated and untreated cells, no anticipation, and pairwise untreated parallel trends across the treated-versus-never, early-versus-late, and late-versus-early comparison types; then the two-way fixed-effects coefficient betaTWFE P equals the sum, over admissible pairwise comparisons, of each comparison's Goodman-Bacon weight times its potential-outcome window contrast — the treated-versus-never and early-versus-late window-specific ATTs, or the late-versus-early bad-comparison adjustment.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
contrast_eq_contrastCausaltheorem — On an admissible comparison, the algebraic contrast equals the causal potential-outcome contrast, by the Layer C corollaries.hypotheses𝒢 :sharedType u_1T :sharedℕP :CohortPanel 𝒢 TY0 Y1 :𝒢 → Fin T → ℝhA :CausalAssumptions P Y0 Y1k :CompTag × 𝒢 × 𝒢hk :admissible P kconclusioncontrast P k = contrastCausal P Y0 Y1 kProof (Lean source)
theorem contrast_eq_contrastCausal (P : CohortPanel 𝒢 T) (Y0 Y1 : 𝒢 → Fin T → ℝ) (hA : CausalAssumptions P Y0 Y1) {k : CompTag × 𝒢 × 𝒢} (hk : admissible P k) : contrast P k = contrastCausal P Y0 Y1 k := by unfold contrast contrastCausal rw [if_pos hk, if_pos hk] rcases k with ⟨tag, g, u⟩ cases tag · obtain ⟨hg, hu, _, _⟩ := hk exact Δ_TN_eq_ATT_totalized P Y0 Y1 hA g u hg hu · obtain ⟨hlt, hfin, _, _⟩ := hk exact Δ_EL_eq_ATT_totalized P Y0 Y1 hA g u hlt hfin · obtain ⟨hlt, hfin, _, _⟩ := hk simpa using Δ_LE_eq_bad_comparison P Y0 Y1 hA g u hlt hfin
PopulationBridge 3 core · 0 supporting This file states a conditional transport bridge from a probability-space panel model to the finite Goodman-Bacon cohort-period algebra. ★ bridge_Dtilde_sq_eq_VD_of_residual_compatibility★ bridge_VD_pos_iff_Dtilde_sq_pos_of_residual_compatibility★ bridge_finite_residualized_eq_twfe_of_residual_compatibility
Goodman-Bacon Measure-Theoretic Bridge
This file states a conditional transport bridge from a probability-space panel model to the finite Goodman-Bacon cohort-period algebra. It assumes explicit compatibility between the population and finite residualized treatments; it does not derive that compatibility from an observed staggered-adoption path. Under that premise and the balanced cohort-period law, it identifies the population residualized coefficient with the finite-cell TWFE coefficient.
The population second moment of residualized treatment equals the corresponding finite cohort-period denominator for a probability law with treatment and outcome variables, cohort and period labels, and an adoption schedule, provided the labels and treatment are measurable, treatment is binary almost everywhere, the cohort-period law is balanced, there is at least one period, cohort masses are positive and sum to one, each cohort's mass is uniform across periods, treatment is constant at its mean within every cell, and population and finite residualized treatments agree in every cell.
Formal statement
Proof (Lean source)
Positivity of the finite-panel treatment denominator is equivalent to positivity of the population residualized-treatment second moment for a probability law with treatment and outcome variables, cohort and period labels, and an adoption schedule, provided the labels and treatment are measurable, treatment is binary almost everywhere, the cohort-period law is balanced, there is at least one period, cohort masses are positive and sum to one, each cohort's mass is uniform across periods, treatment is constant at its mean within every cell, and population and finite residualized treatments agree in every cell.
Formal statement
Proof (Lean source)
The population coefficient from residualizing treatment and outcome on cohort and period effects equals the induced finite-panel TWFE coefficient for a probability law with treatment and outcome variables, cohort and period labels, and an adoption schedule, provided the labels and treatment are measurable, treatment is binary almost everywhere, the outcome is square-integrable, the cohort-period law is balanced, there is at least one period, cohort masses are positive and sum to one, each cohort's mass is uniform across periods, treatment is constant at its mean within every cell, and population and finite residualized treatments agree in every cell.