Panel.EstimandCharacterization.StaggeredTWFEDecomposition
The Goodman-Bacon decomposition: TWFE-DiD as a weighted average of 2x2 comparisons, with the weight formulas.
FinitePanel 38 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 an adoption date and a panel period, the adopted-by-period condition holds exactly when the adoption date is no later than that period; a never-adopting cohort does not satisfy it.
For an adoption date and a panel period, the untreated-at-period condition holds exactly when the period precedes the adoption date, including every period for a never-adopting cohort.
For an adoption date, the eventually-treated condition holds exactly when the date is a finite panel period rather than the never-adopting value.
For an adoption date, the never-treated condition holds exactly when the date is the never-adopting value.
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.
For a never-treated potential-outcome schedule, a cohort, and a set of periods, the never-treated potential-outcome window mean is the average of that cohort's never-treated potential outcomes over the specified periods; it is defined as zero when the set is empty.
For the never-treated potential-outcome schedule, the own-adoption potential-outcome schedule, a cohort, and a set of periods, the window-specific average treatment effect on the treated is the average over the specified periods of the own-adoption potential outcome minus the never-treated potential outcome for that cohort; it is defined as zero when the set is empty.
Causal-side assumptions for the Goodman-Bacon decomposition (LaTeX ass:po-estimand-goodman-bacon-causal), given a cohort panel P and potential-outcome maps Y0 (the never-treated path) and Y1 (each cohort's own adoption-date path). It packages consistency on treated cells — the factual outcome equals the post-adoption potential outcome once the cohort has adopted, consistency on untreated cells — the factual outcome equals the never-treated potential outcome before adoption, no anticipation — the pre-adoption potential outcomes under the two paths coincide, and pairwise untreated parallel trends for the treated-versus-never comparison, the early-versus-late-before-late comparison, and the late-versus-early-after-early comparison.
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).
Layer C corollary 1 — TN identifies ATT. Fix a cohort panel P and potential-outcome maps Y0 (never-treated path) and Y1 (own-adoption-date path), and assume consistency on treated and untreated cells, no anticipation, and pairwise untreated parallel trends across the three comparison types. For a treated cohort g whose adoption date is finite compared against a never-treated cohort u whose adoption date is infinite, the treated-versus-never 2x2 difference-in-differences contrast Δ_TN equals g's window-specific average treatment effect on the treated over its post-adoption window:
Formal statement
Proof (Lean source)
Layer C corollary 2 — EL identifies the early cohort's ATT. 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 early-versus-late contrast Δ_EL equals e's window-specific average treatment effect on the treated over the window running from e's own adoption date up to ℓ's adoption date:
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)
-
not_le_of_lttheorem — Helper: AdoptionDate.lt (P.A g) t rules out AdoptionDate.le (P.A g) t.hypothesesconclusion¬ AdoptionDate.le a tProof (Lean source)
theorem AdoptionDate.not_le_of_lt {a : WithTop (Fin T)} {t : Fin T} (h : AdoptionDate.lt a t) : ¬ AdoptionDate.le a t := by intro hle exact lt_irrefl _ (lt_of_lt_of_le h hle) -
lt_of_isInftheorem — Helper: every period is strictly less than ⊤ in WithTop (Fin T). -
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 tifAdoptionDate.lt (P.A g) tthenP.Y g t = Y0 g tg :𝒢Proof (Lean source)
theorem Ybar_eq_Ybar0_on_S0_TN (hConsistency : ∀ g t, AdoptionDate.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 : AdoptionDate.lt (P.A g) t := by simpa [S0_TN, mem_filter] 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 tifAdoptionDate.lt (P.A g) tthenP.Y g t = Y0 g tu :𝒢hS :∀ t ∈ S, AdoptionDate.lt (P.A u) tProof (Lean source)
theorem Ybar_eq_Ybar0_of_inf (hConsistency : ∀ g t, AdoptionDate.lt (P.A g) t → P.Y g t = Y0 g t) {u : 𝒢} (S : Finset (Fin T)) (hS : ∀ t ∈ S, AdoptionDate.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 tifAdoptionDate.le (P.A g) tthenP.Y g t = Y1 g tg :𝒢hS :∀ t ∈ S, AdoptionDate.le (P.A g) tconclusionProof (Lean source)
theorem Ybar_eq_Ybar0_add_ATT_of_treated (hConsistency : ∀ g t, AdoptionDate.le (P.A g) t → P.Y g t = Y1 g t) (g : 𝒢) (S : Finset (Fin T)) (hS : ∀ t ∈ S, AdoptionDate.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 tifAdoptionDate.lt (P.A g) tthenP.Y g t = Y0 g te :𝒢Proof (Lean source)
theorem Ybar_eq_Ybar0_on_S0_EL (hConsistency : ∀ g t, AdoptionDate.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 : AdoptionDate.lt (P.A e) t := by simpa [S0_EL, mem_filter] 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 tifAdoptionDate.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, AdoptionDate.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 : AdoptionDate.le (P.A e) t ∧ AdoptionDate.lt (P.A ℓ) t := by simpa [S1_EL, mem_filter] 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 tifAdoptionDate.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, AdoptionDate.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 : AdoptionDate.lt (P.A e) t := by simpa [S0_EL, mem_filter] using ht exact h0 exact hConsistency ℓ t (by simpa [AdoptionDate.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 tifAdoptionDate.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, AdoptionDate.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 : AdoptionDate.le (P.A e) t ∧ AdoptionDate.lt (P.A ℓ) t := by simpa [S0_LE, S1_EL, mem_filter] using ht exact hConsistency ℓ t htmem.2
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, the two-way fixed-effects (TWFE) coefficient, under the totalized zero-variance convention, equals the weighted sum of admissible two-by-two DID contrasts across comparison groups.
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 : AdoptionDate.isInf (P.A g)) : barD P g = 0 := by unfold barD D AdoptionDate.isInf AdoptionDate.le at * simp [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 : AdoptionDate.isInf (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 AdoptionDate.isFin (P.A g) ∧ AdoptionDate.isInf (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 ℓ ∧ AdoptionDate.isFin (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 AdoptionDate.isFin (P.A g) ∧ AdoptionDate.isInf (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 ℓ ∧ AdoptionDate.isFin (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 : AdoptionDate.isFin (P.A g) ∧ AdoptionDate.isInf (P.A u) · simp [h, lambdaTN_eq_gap_of_isInf P h.2] · simp [h] · refine Finset.sum_congr rfl ?_ intro e _he refine Finset.sum_congr rfl ?_ intro ℓ _hℓ by_cases h : P.A e < P.A ℓ ∧ AdoptionDate.isFin (P.A ℓ) · simp [h, lambdaEL_add_lambdaLE_eq_gap P e ℓ] · simp [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 AdoptionDate.isFin (P.A g) ∧ AdoptionDate.isInf (P.A u) then f g u else 0)+ (∑ g, ∑ u, if AdoptionDate.isFin (P.A u) ∧ AdoptionDate.isInf (P.A g) then f g u else 0)+ (∑ g, ∑ u, if P.A g < P.A u ∧ AdoptionDate.isFin (P.A u) then f g u else 0)+ (∑ g, ∑ u, if P.A u < P.A g ∧ AdoptionDate.isFin (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 AdoptionDate.isFin (P.A g) ∧ AdoptionDate.isInf (P.A u) then f g u else 0) + (∑ g, ∑ u, if AdoptionDate.isFin (P.A u) ∧ AdoptionDate.isInf (P.A g) then f g u else 0) + (∑ g, ∑ u, if P.A g < P.A u ∧ AdoptionDate.isFin (P.A u) then f g u else 0) + (∑ g, ∑ u, if P.A u < P.A g ∧ AdoptionDate.isFin (P.A g) then f g u else 0) := by calc (∑ g, ∑ u, f g u) = ∑ g, ∑ u, ((if AdoptionDate.isFin (P.A g) ∧ AdoptionDate.isInf (P.A u) then f g u else 0) + (if AdoptionDate.isFin (P.A u) ∧ AdoptionDate.isInf (P.A g) then f g u else 0) + (if P.A g < P.A u ∧ AdoptionDate.isFin (P.A u) then f g u else 0) + (if P.A u < P.A g ∧ AdoptionDate.isFin (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 AdoptionDate.isFin (P.A g) ∧ AdoptionDate.isInf (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 ℓ ∧ AdoptionDate.isFin (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 AdoptionDate.isFin (P.A g) ∧ AdoptionDate.isInf (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 ℓ ∧ AdoptionDate.isFin (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 : AdoptionDate.isFin (P.A g) ∧ AdoptionDate.isInf (P.A u) · simp [h, TN_pair_vd_contribution_eq_gap P h.2] · simp [h] · refine Finset.sum_congr rfl ?_ intro e _he refine Finset.sum_congr rfl ?_ intro ℓ _hℓ by_cases h : P.A e < P.A ℓ ∧ AdoptionDate.isFin (P.A ℓ) · simp [h, TT_pair_vd_contribution_eq_gap P h.1] · simp [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.hypothesesconclusionProof (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 AdoptionDate.isFin (P.A g) ∧ AdoptionDate.isInf (P.A u) then lambdaTN P g u * Δ_TN P g u else 0) + (∑ e, ∑ ℓ, if P.A e < P.A ℓ ∧ AdoptionDate.isFin (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 : AdoptionDate.isFin (P.A g) ∧ AdoptionDate.isInf (P.A u) · simp [h, TN_pair_contribution_eq_lambda_delta P h.1 h.2] · simp [h] · refine Finset.sum_congr rfl ?_ intro e _he refine Finset.sum_congr rfl ?_ intro ℓ _hℓ by_cases h : P.A e < P.A ℓ ∧ AdoptionDate.isFin (P.A ℓ) · simp [h, TT_pair_contribution_eq_lambda_delta_sum P h.1 h.2] · simp [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 ℓ ∧ AdoptionDate.isFin (P.A ℓ) then lambdaEL P e ℓ else 0) + (∑ e, ∑ ℓ, if P.A e < P.A ℓ ∧ AdoptionDate.isFin (P.A ℓ) then lambdaLE P e ℓ else 0) = ∑ e, ∑ ℓ, if P.A e < P.A ℓ ∧ AdoptionDate.isFin (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 ℓ ∧ AdoptionDate.isFin (P.A ℓ) <;> simp [h] unfold Lambda rw [← hELLE] rw [add_assoc] -
twfe_eq_weighted_avg_coretheorem — The positivity-free algebraic core of the Goodman-Bacon decomposition: the totalized TWFE ratio equals the totalized weighted sum of admissible two-by-two DID contrasts, including in zero-variance cases.hypothesesProof (Lean source)
theorem twfe_eq_weighted_avg_core (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 AdoptionDate.isFin (P.A g) ∧ AdoptionDate.isInf (P.A u) then lambdaTN P g u * Δ_TN P g u else 0) + (∑ e, ∑ ℓ, if P.A e < P.A ℓ ∧ AdoptionDate.isFin (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-ATT corollaries, expressing the two-way fixed-effect coefficient as a sum of normalized comparison weights times potential-outc ★ twfe_po_decomposition
Goodman-Bacon fused causal decomposition
This file composes the algebraic TWFE totalized weighted-sum identity with the
causal window-ATT corollaries, 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. 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 P Y0 Y1 hA g u hg hu · obtain ⟨hlt, hfin, _, _⟩ := hk exact Δ_EL_eq_ATT 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
Pairwise 5 core · 13 supporting This file reduces Goodman-Bacon denominator and numerator terms to ordered-pair centered-treatment contributions. ★ VD_eq_pairwise_centeredD★ TN_pair_contribution_eq_lambda_delta
Goodman-Bacon Pairwise Algebra
This file reduces Goodman-Bacon denominator and numerator terms to ordered-pair centered-treatment contributions. It is the algebraic bridge between generic finite weighted covariance identities and the adoption-window case analysis that produces the three comparison types in the decomposition.
For a cohort panel, a cohort, and a period, the cohort-demeaned treatment path is that cohort's treatment indicator in the period minus its average treatment indicator across all periods.
Definition (Lean source)
For a cohort panel and two cohorts, the ordered-pair contribution to residualized-treatment variance is one half of their share product divided by the number of periods, multiplied by the sum of squared differences between their cohort-demeaned treatment paths.
Definition (Lean source)
For a cohort panel and two cohorts, the ordered-pair contribution to the two-way-fixed-effects numerator is one half of their share product divided by the number of periods, multiplied by the sum of the product of their demeaned-treatment difference and factual-outcome difference.
Definition (Lean source)
For a cohort panel, the residualized-treatment variance VD P equals the sum, over all ordered pairs of cohorts, of their pairwise centered-treatment contribution vdPairContribution P g u.
Formal statement
Proof (Lean source)
TN numerator pair. For a treated cohort g with finite adoption date and a never-treated cohort u with infinite adoption date, the sum of the two ordered pairwise-covariance contributions between g and u in the finite cohort panel P equals the product of the TN comparison weight and the treated-versus-never contrast, λ_TN P g u · Δ_TN P g u.
Formal statement
Proof (Lean source)
13 supporting declarations (lemmas, instances)
-
weighted_center_cov_uncentered_rightlemma — For a finite collection with weights summing to one, the weighted sum of deviations of one quantity from its weighted mean times another quantity equals one half of the weighted sum of pairwise differences in the two quantities.hypothesesconclusion∑ i, p i * (x i - ∑ j, p j * x j) * y i= (1 / 2) * ∑ i, ∑ j, p i * p j * (x i - x j) * (y i - y j)Proof (Lean source)
lemma weighted_center_cov_uncentered_right {ι : Type*} [Fintype ι] (p x y : ι → ℝ) (hp : ∑ i, p i = 1) : ∑ i, p i * (x i - ∑ j, p j * x j) * y i = (1 / 2) * ∑ i, ∑ j, p i * p j * (x i - x j) * (y i - y j) := by classical let mx := ∑ j, p j * x j let my := ∑ j, p j * y j have hzero : ∑ i, p i * (x i - mx) = 0 := by calc ∑ i, p i * (x i - mx) = (∑ i, p i * x i) - ∑ i, p i * mx := by simp [mul_sub, Finset.sum_sub_distrib] _ = mx - (∑ i, p i) * mx := by simp [Finset.sum_mul, mx] _ = 0 := by rw [hp] ring have hmy : ∑ i, p i * (x i - mx) * my = 0 := by calc ∑ i, p i * (x i - mx) * my = (∑ i, p i * (x i - mx)) * my := by rw [Finset.sum_mul] _ = 0 := by rw [hzero] ring have hcenter : ∑ i, p i * (x i - mx) * y i = ∑ i, p i * (x i - mx) * (y i - my) := by calc ∑ i, p i * (x i - mx) * y i = ∑ i, (p i * (x i - mx) * (y i - my) + p i * (x i - mx) * my) := by refine Finset.sum_congr rfl ?_ intro i _hi ring _ = ∑ i, p i * (x i - mx) * (y i - my) + ∑ i, p i * (x i - mx) * my := by rw [Finset.sum_add_distrib] _ = ∑ i, p i * (x i - mx) * (y i - my) := by rw [hmy] ring calc ∑ i, p i * (x i - ∑ j, p j * x j) * y i = ∑ i, p i * (x i - mx) * y i := by rfl _ = ∑ i, p i * (x i - mx) * (y i - my) := hcenter _ = ∑ i, p i * (x i - ∑ j, p j * x j) * (y i - ∑ j, p j * y j) := by rfl _ = (1 / 2) * ∑ i, ∑ j, p i * p j * (x i - x j) * (y i - y j) := weighted_center_cov p x y hp (by norm_num) -
sum_weight_over_T_commutelemma — In a finite cohort panel, a cohort-weighted sum over cohorts and periods with equal period weight equals the average over periods of the corresponding cohort-weighted sums.hypothesesconclusion(∑ g, ∑ t, (P.p g / (T : ℝ)) * f g t) = (T : ℝ)⁻¹ * ∑ t, ∑ g, P.p g * f g tProof (Lean source)
lemma sum_weight_over_T_commute (P : CohortPanel 𝒢 T) (f : 𝒢 → Fin T → ℝ) : (∑ g, ∑ t, (P.p g / (T : ℝ)) * f g t) = (T : ℝ)⁻¹ * ∑ t, ∑ g, P.p g * f g t := by classical rw [Finset.sum_comm] simp [div_eq_mul_inv, Finset.mul_sum, mul_left_comm, mul_comm] -
pairwise_sum_normalizelemma — In a finite cohort panel, averaging half the ordered-pair weighted total at each period equals the ordered-pair weighted total of the time sums with the same normalization.hypothesesconclusion(T : ℝ)⁻¹ * ∑ t, ((1 / 2) * ∑ g, ∑ u, P.p g * P.p u * f g u t)= ∑ g, ∑ u, (P.p g * P.p u / (2 * (T : ℝ))) * ∑ t, f g u tProof (Lean source)
lemma pairwise_sum_normalize (P : CohortPanel 𝒢 T) (f : 𝒢 → 𝒢 → Fin T → ℝ) : (T : ℝ)⁻¹ * ∑ t, ((1 / 2) * ∑ g, ∑ u, P.p g * P.p u * f g u t) = ∑ g, ∑ u, (P.p g * P.p u / (2 * (T : ℝ))) * ∑ t, f g u t := by classical calc (T : ℝ)⁻¹ * ∑ t, ((1 / 2) * ∑ g, ∑ u, P.p g * P.p u * f g u t) = (T : ℝ)⁻¹ * ∑ t, ∑ g, ∑ u, (1 / 2) * (P.p g * P.p u * f g u t) := by simp [Finset.mul_sum] _ = (T : ℝ)⁻¹ * ∑ g, ∑ u, ∑ t, (1 / 2) * (P.p g * P.p u * f g u t) := by congr 1 rw [Finset.sum_comm] refine Finset.sum_congr rfl ?_ intro g _hg rw [Finset.sum_comm] _ = ∑ g, ∑ u, (P.p g * P.p u / (2 * (T : ℝ))) * ∑ t, f g u t := by simp [div_eq_mul_inv, Finset.mul_sum, Finset.sum_mul, mul_assoc, mul_left_comm, mul_comm] -
D_eq_zero_of_isInflemma — In a cohort panel, a cohort that is never treated has a zero treatment indicator in every period.hypotheses𝒢 :sharedType u_1T :sharedℕP :CohortPanel 𝒢 Tu :𝒢hu :AdoptionDate.isInf (P.A u)t :Fin TconclusionD P u t = 0Proof (Lean source)
lemma D_eq_zero_of_isInf (P : CohortPanel 𝒢 T) {u : 𝒢} (hu : AdoptionDate.isInf (P.A u)) (t : Fin T) : D P u t = 0 := by classical unfold D rw [show P.A u = ⊤ from hu] simp [AdoptionDate.le] -
D_sq_eq_Dlemma — In a cohort panel, the binary treatment indicator for any cohort and time period equals its own square.hypothesesconclusionD P g t ^ 2 = D P g tProof (Lean source)
lemma D_sq_eq_D (P : CohortPanel 𝒢 T) (g : 𝒢) (t : Fin T) : D P g t ^ 2 = D P g t := by unfold D by_cases h : AdoptionDate.le (P.A g) t <;> simp [h] -
binary_time_variancelemma — For a binary quantity observed over the panel's time periods, its average squared deviation from its time mean equals that mean times one minus that mean.hypothesesconclusion(T : ℝ)⁻¹ * ∑ t, (x t - ((T : ℝ)⁻¹ * ∑ t, x t)) ^ 2= ((T : ℝ)⁻¹ * ∑ t, x t) * (1 - ((T : ℝ)⁻¹ * ∑ t, x t))Proof (Lean source)
lemma binary_time_variance (hT_pos : 0 < T) (x : Fin T → ℝ) (hx : ∀ t, x t ^ 2 = x t) : (T : ℝ)⁻¹ * ∑ t, (x t - ((T : ℝ)⁻¹ * ∑ t, x t)) ^ 2 = ((T : ℝ)⁻¹ * ∑ t, x t) * (1 - ((T : ℝ)⁻¹ * ∑ t, x t)) := by classical let m : ℝ := (T : ℝ)⁻¹ * ∑ t, x t have hTne : (T : ℝ) ≠ 0 := by exact_mod_cast (ne_of_gt hT_pos) have hsum_sq : ∑ t, x t ^ 2 = ∑ t, x t := by exact Finset.sum_congr rfl (by intro t _ht; exact hx t) have hsum_expand : ∑ t, (x t ^ 2 - 2 * m * x t + m ^ 2) = ∑ t, x t - 2 * m * ∑ t, x t + (T : ℝ) * m ^ 2 := by calc ∑ t, (x t ^ 2 - 2 * m * x t + m ^ 2) = ∑ t, x t ^ 2 - ∑ t, 2 * m * x t + ∑ _t : Fin T, m ^ 2 := by simp [Finset.sum_sub_distrib, Finset.sum_add_distrib] _ = ∑ t, x t - 2 * m * ∑ t, x t + (T : ℝ) * m ^ 2 := by rw [hsum_sq] simp [Finset.mul_sum, Fintype.card_fin] calc (T : ℝ)⁻¹ * ∑ t, (x t - ((T : ℝ)⁻¹ * ∑ t, x t)) ^ 2 = (T : ℝ)⁻¹ * ∑ t, (x t ^ 2 - 2 * m * x t + m ^ 2) := by congr 1 refine Finset.sum_congr rfl ?_ intro t _ht simp [m] ring _ = ((T : ℝ)⁻¹ * ∑ t, x t) * (1 - ((T : ℝ)⁻¹ * ∑ t, x t)) := by rw [hsum_expand] simp [m] field_simp [hTne] ring -
binary_time_cov_filter_meanlemma — For an indicator of a nonempty set of periods, the time-average product of its centered value and another quantity equals its variance times the difference between the selected-period and unselected-period averages of that quantity.hypothesesT :sharedℕhT_pos :0 < Tp :Fin T → Propz :Fin T → ℝhcard1 :((Finset.univ.filter p).card : ℝ) ≠ 0conclusion(T : ℝ)⁻¹ * ∑ t, ((if p t then (1 : ℝ) else 0) - ((T : ℝ)⁻¹ * ∑ t, (if p t then (1 : ℝ) else 0))) * z t= ((T : ℝ)⁻¹ * ∑ t, (if p t then (1 : ℝ) else 0)) * (1 - ((T : ℝ)⁻¹ * ∑ t, (if p t then (1 : ℝ) else 0))) * (((Finset.univ.filter p).card : ℝ)⁻¹ * (∑ t ∈ (Finset.univ.filter p), z t) - ((Finset.univ.filter (fun t => ¬ p t)).card : ℝ)⁻¹ * (∑ t ∈ (Finset.univ.filter (fun t => ¬ p t)), z t))Proof (Lean source)
lemma binary_time_cov_filter_mean (hT_pos : 0 < T) (p : Fin T → Prop) [DecidablePred p] (z : Fin T → ℝ) (hcard1 : ((Finset.univ.filter p).card : ℝ) ≠ 0) : (T : ℝ)⁻¹ * ∑ t, ((if p t then (1 : ℝ) else 0) - ((T : ℝ)⁻¹ * ∑ t, (if p t then (1 : ℝ) else 0))) * z t = ((T : ℝ)⁻¹ * ∑ t, (if p t then (1 : ℝ) else 0)) * (1 - ((T : ℝ)⁻¹ * ∑ t, (if p t then (1 : ℝ) else 0))) * (((Finset.univ.filter p).card : ℝ)⁻¹ * (∑ t ∈ (Finset.univ.filter p), z t) - ((Finset.univ.filter (fun t => ¬ p t)).card : ℝ)⁻¹ * (∑ t ∈ (Finset.univ.filter (fun t => ¬ p t)), z t)) := by classical have hTne : (T : ℝ) ≠ 0 := by exact_mod_cast (ne_of_gt hT_pos) let A : ℝ := ((Finset.univ.filter p).card : ℝ) let B : ℝ := ((Finset.univ.filter (fun t => ¬ p t)).card : ℝ) let Z1 : ℝ := ∑ t ∈ (Finset.univ.filter p), z t let Z0 : ℝ := ∑ t ∈ (Finset.univ.filter (fun t => ¬ p t)), z t have hA : A ≠ 0 := by simpa [A] using hcard1 have hsum_if : (∑ t, (if p t then (1 : ℝ) else 0)) = A := by simp [A] have hsum_if_z : (∑ t, (if p t then (1 : ℝ) else 0) * z t) = Z1 := by simp [Z1, Finset.sum_filter] have hsum_z : (∑ t, z t) = Z1 + Z0 := by simp [Z1, Z0, Finset.sum_filter] rw [← Finset.sum_add_distrib] refine Finset.sum_congr rfl ?_ intro t _ by_cases ht : p t <;> simp [ht] have hcard_total : A + B = (T : ℝ) := by have hnat : (Finset.univ.filter p).card + (Finset.univ.filter (fun t => ¬ p t)).card = T := by calc (Finset.univ.filter p).card + (Finset.univ.filter (fun t => ¬ p t)).card = ((Finset.univ.filter p) ∪ (Finset.univ.filter (fun t => ¬ p t))).card := by rw [Finset.card_union_of_disjoint] simp [Finset.disjoint_left] _ = T := by have hunion : (Finset.univ.filter p) ∪ (Finset.univ.filter (fun t => ¬ p t)) = (Finset.univ : Finset (Fin T)) := by ext t simp [em] simp [hunion] simpa [A, B] using (show (((Finset.univ.filter p).card : ℝ) + ((Finset.univ.filter (fun t => ¬ p t)).card : ℝ) = (T : ℝ)) by exact_mod_cast hnat) have hmain : (T : ℝ)⁻¹ * (Z1 - ((T : ℝ)⁻¹ * A) * (Z1 + Z0)) = ((T : ℝ)⁻¹ * A) * (1 - ((T : ℝ)⁻¹ * A)) * (A⁻¹ * Z1 - B⁻¹ * Z0) := by by_cases hB : B = 0 · have hZT0 : Z0 = 0 := by have hempty : Finset.univ.filter (fun t => ¬ p t) = ∅ := by apply Finset.card_eq_zero.mp have hB' : ((Finset.univ.filter (fun t => ¬ p t)).card : ℝ) = 0 := by simpa [B] using hB exact_mod_cast hB' simp [Z0, hempty] have hAeq : A = (T : ℝ) := by linarith rw [hZT0, hAeq] field_simp [hTne] ring · have hABne : A + B ≠ 0 := by rw [hcard_total] exact hTne rw [← hcard_total] field_simp [hA, hB, hABne] ring calc (T : ℝ)⁻¹ * ∑ t, ((if p t then (1 : ℝ) else 0) - ((T : ℝ)⁻¹ * ∑ t, (if p t then (1 : ℝ) else 0))) * z t = (T : ℝ)⁻¹ * (Z1 - ((T : ℝ)⁻¹ * A) * (Z1 + Z0)) := by rw [hsum_if] calc (T : ℝ)⁻¹ * ∑ t, ((if p t then (1 : ℝ) else 0) - (T : ℝ)⁻¹ * A) * z t = (T : ℝ)⁻¹ * (∑ t, (if p t then (1 : ℝ) else 0) * z t - ∑ t, ((T : ℝ)⁻¹ * A) * z t) := by congr 1 rw [← Finset.sum_sub_distrib] refine Finset.sum_congr rfl ?_ intro t _ ring _ = (T : ℝ)⁻¹ * (Z1 - ((T : ℝ)⁻¹ * A) * (Z1 + Z0)) := by rw [hsum_if_z, ← Finset.mul_sum, hsum_z] _ = ((T : ℝ)⁻¹ * ∑ t, (if p t then (1 : ℝ) else 0)) * (1 - ((T : ℝ)⁻¹ * ∑ t, (if p t then (1 : ℝ) else 0))) * (((Finset.univ.filter p).card : ℝ)⁻¹ * (∑ t ∈ (Finset.univ.filter p), z t) - ((Finset.univ.filter (fun t => ¬ p t)).card : ℝ)⁻¹ * (∑ t ∈ (Finset.univ.filter (fun t => ¬ p t)), z t)) := by rw [hmain, hsum_if] -
Dtilde_eq_centeredD_sub_weighted_meanlemma — The explicit double-demeaning formula for Dtilde is the weighted centering, across cohorts, of the cohort-demeaned treatment path.hypothesesProof (Lean source)
lemma Dtilde_eq_centeredD_sub_weighted_mean (P : CohortPanel 𝒢 T) (g : 𝒢) (t : Fin T) : Dtilde P g t = centeredD P g t - ∑ h, P.p h * centeredD P h t := by rw [weighted_centeredD_mean P t] rw [Dtilde_eq] unfold centeredD ring -
twfe_numerator_eq_pairwise_centeredD_Ylemma — Pairwise representation of the TWFE numerator.hypothesesconclusion(∑ g, ∑ t, (P.p g / (T : ℝ)) * Dtilde P g t * P.Y g t)= ∑ g, ∑ u, numPairContribution P g uProof (Lean source)
lemma twfe_numerator_eq_pairwise_centeredD_Y (P : CohortPanel 𝒢 T) : (∑ g, ∑ t, (P.p g / (T : ℝ)) * Dtilde P g t * P.Y g t) = ∑ g, ∑ u, numPairContribution P g u := by classical calc (∑ g, ∑ t, (P.p g / (T : ℝ)) * Dtilde P g t * P.Y g t) = ∑ g, ∑ t, (P.p g / (T : ℝ)) * (Dtilde P g t * P.Y g t) := by refine Finset.sum_congr rfl ?_ intro g _hg refine Finset.sum_congr rfl ?_ intro t _ht ring _ = (T : ℝ)⁻¹ * ∑ t, ∑ g, P.p g * (Dtilde P g t * P.Y g t) := by exact sum_weight_over_T_commute P (fun g t => Dtilde P g t * P.Y g t) _ = (T : ℝ)⁻¹ * ∑ t, ∑ g, P.p g * (centeredD P g t - ∑ h, P.p h * centeredD P h t) * P.Y g t := by congr 1 refine Finset.sum_congr rfl ?_ intro t _ht refine Finset.sum_congr rfl ?_ intro g _hg rw [Dtilde_eq_centeredD_sub_weighted_mean] ring _ = (T : ℝ)⁻¹ * ∑ t, ((1 / 2) * ∑ g, ∑ u, P.p g * P.p u * (centeredD P g t - centeredD P u t) * (P.Y g t - P.Y u t)) := by congr 1 refine Finset.sum_congr rfl ?_ intro t _ht exact weighted_center_cov_uncentered_right (fun g => P.p g) (fun g => centeredD P g t) (fun g => P.Y g t) P.p_sum_one _ = ∑ g, ∑ u, numPairContribution P g u := by unfold numPairContribution simpa [mul_assoc] using pairwise_sum_normalize P (fun g u t => (centeredD P g t - centeredD P u t) * (P.Y g t - P.Y u t)) -
disjoint_union_mean_eq_card_weighted_meanlemma — When two finite sets are disjoint and the second is nonempty, the mean of a quantity over their union is the cardinality-weighted combination of its means over the two sets.hypothesesconclusion(((A ∪ B).card : ℝ)⁻¹ * ∑ t ∈ A ∪ B, z t)= ((A.card : ℝ) / ((A ∪ B).card : ℝ)) * ((A.card : ℝ)⁻¹ * ∑ t ∈ A, z t)+ (1 - ((A.card : ℝ) / ((A ∪ B).card : ℝ))) * ((B.card : ℝ)⁻¹ * ∑ t ∈ B, z t)Proof (Lean source)
lemma disjoint_union_mean_eq_card_weighted_mean {α : Type*} [DecidableEq α] (A B : Finset α) (z : α → ℝ) (hdisj : Disjoint A B) (hB : ((B.card : ℝ) ≠ 0)) : (((A ∪ B).card : ℝ)⁻¹ * ∑ t ∈ A ∪ B, z t) = ((A.card : ℝ) / ((A ∪ B).card : ℝ)) * ((A.card : ℝ)⁻¹ * ∑ t ∈ A, z t) + (1 - ((A.card : ℝ) / ((A ∪ B).card : ℝ))) * ((B.card : ℝ)⁻¹ * ∑ t ∈ B, z t) := by classical let a : ℝ := A.card let b : ℝ := B.card let ZA : ℝ := ∑ t ∈ A, z t let ZB : ℝ := ∑ t ∈ B, z t have hsum : ∑ t ∈ A ∪ B, z t = ZA + ZB := by simp [ZA, ZB, Finset.sum_union hdisj] have hcard : ((A ∪ B).card : ℝ) = a + b := by have hnat : (A ∪ B).card = A.card + B.card := Finset.card_union_of_disjoint hdisj simp [a, b, hnat] have hb : b ≠ 0 := by simpa [b] using hB have hbpos : 0 < b := by have hBnat : B.card ≠ 0 := by exact_mod_cast hB dsimp [b] exact_mod_cast (Nat.pos_of_ne_zero hBnat) have hab : a + b ≠ 0 := by intro h have ha_nonneg : 0 ≤ a := by dsimp [a] exact_mod_cast (zero_le A.card) linarith by_cases ha : a = 0 · have hAempty : A = ∅ := by apply Finset.card_eq_zero.mp have : (A.card : ℝ) = 0 := by simpa [a] using ha exact Nat.cast_eq_zero.mp this have hZA : ZA = 0 := by simp [ZA, hAempty] rw [hsum, hcard, hZA, ha] simp [hAempty] field_simp [hb] ring · have haA : ((A.card : ℝ) ≠ 0) := by simpa [a] using ha have hAB : ((A.card : ℝ) + (B.card : ℝ)) ≠ 0 := by simpa [a, b] using hab rw [hsum, hcard] field_simp [haA, hB, hAB] simp [a, b, ZA, ZB] ring_nf -
TN_pair_vd_contribution_eq_gaplemma — TN denominator pair: combining the two ordered pairwise-variance contributions gives the treated-vs-never raw denominator factor.hypothesesconclusionvdPairContribution P g u + vdPairContribution P u g= P.p g * P.p u * q P g u * (1 - q P g u)Proof (Lean source)
lemma TN_pair_vd_contribution_eq_gap (P : CohortPanel 𝒢 T) {g u : 𝒢} (hu : AdoptionDate.isInf (P.A u)) : vdPairContribution P g u + vdPairContribution P u g = P.p g * P.p u * q P g u * (1 - q P g u) := by rw [vdPairContribution_add_swap] have hTne : (T : ℝ) ≠ 0 := by exact_mod_cast (ne_of_gt P.T_pos) have hvar := TN_time_variance_eq_gap P (g := g) hu calc (P.p g * P.p u / (T : ℝ)) * ∑ t, (centeredD P g t - centeredD P u t)^2 = P.p g * P.p u * ((T : ℝ)⁻¹ * ∑ t, (centeredD P g t - centeredD P u t)^2) := by field_simp [hTne] _ = P.p g * P.p u * q P g u * (1 - q P g u) := by rw [hvar] ring -
TT_pair_vd_contribution_eq_gaplemma — Treated-treated denominator pair: combining the two ordered pairwise-variance contributions gives the timing-pair raw denominator factor.hypothesesconclusionvdPairContribution P e ℓ + vdPairContribution P ℓ e= P.p e * P.p ℓ * q P e ℓ * (1 - q P e ℓ)Proof (Lean source)
lemma TT_pair_vd_contribution_eq_gap (P : CohortPanel 𝒢 T) {e ℓ : 𝒢} (hord : P.A e < P.A ℓ) : vdPairContribution P e ℓ + vdPairContribution P ℓ e = P.p e * P.p ℓ * q P e ℓ * (1 - q P e ℓ) := by rw [vdPairContribution_add_swap] have hTne : (T : ℝ) ≠ 0 := by exact_mod_cast (ne_of_gt P.T_pos) have hvar := TT_time_variance_eq_gap P hord calc (P.p e * P.p ℓ / (T : ℝ)) * ∑ t, (centeredD P e t - centeredD P ℓ t)^2 = P.p e * P.p ℓ * ((T : ℝ)⁻¹ * ∑ t, (centeredD P e t - centeredD P ℓ t)^2) := by field_simp [hTne] _ = P.p e * P.p ℓ * q P e ℓ * (1 - q P e ℓ) := by rw [hvar] ring -
TT_pair_contribution_eq_lambda_delta_sumlemma — Treated-treated numerator pair: combining the two ordered pairwise-covariance contributions splits into the EL and LE comparison windows.hypotheses𝒢 :sharedType u_1T :sharedℕP :CohortPanel 𝒢 Te ℓ :𝒢hord :P.A e < P.A ℓhℓ :AdoptionDate.isFin (P.A ℓ)conclusionnumPairContribution P e ℓ + numPairContribution P ℓ eProof (Lean source)
lemma TT_pair_contribution_eq_lambda_delta_sum (P : CohortPanel 𝒢 T) {e ℓ : 𝒢} (hord : P.A e < P.A ℓ) (hℓ : AdoptionDate.isFin (P.A ℓ)) : numPairContribution P e ℓ + numPairContribution P ℓ e = lambdaEL P e ℓ * Δ_EL P e ℓ + lambdaLE P e ℓ * Δ_LE P e ℓ := by rw [numPairContribution_add_swap] have hTne : (T : ℝ) ≠ 0 := by exact_mod_cast (ne_of_gt P.T_pos) have hcov := TT_time_cov_eq_lambda_delta_core P hord hℓ calc (P.p e * P.p ℓ / (T : ℝ)) * ∑ t, (centeredD P e t - centeredD P ℓ t) * (P.Y e t - P.Y ℓ t) = P.p e * P.p ℓ * ((T : ℝ)⁻¹ * ∑ t, (centeredD P e t - centeredD P ℓ t) * (P.Y e t - P.Y ℓ t)) := by field_simp [hTne] _ = lambdaEL P e ℓ * Δ_EL P e ℓ + lambdaLE P e ℓ * Δ_LE P e ℓ := by rw [hcov] unfold lambdaEL lambdaLE ring
PopulationBridge 3 core · 0 supporting This file states the public bridge from a probability-space panel model to the finite Goodman-Bacon cohort-period algebra. ★ bridge_Dtilde_sq_eq_VD★ bridge_VD_pos_iff_Dtilde_sq_pos★ bridge_finite_residualized_eq_twfe
Goodman-Bacon Measure-Theoretic Bridge
This file states the public bridge from a probability-space panel model to the finite Goodman-Bacon cohort-period algebra. It relates residualized-treatment integrals to the finite-panel denominator and numerator, allowing the abstract residualized coefficient to be read as the finite-cell TWFE coefficient under the balanced cohort-period law.
On a probability space carrying cohort label G, period label T_rv, treatment D, and outcome Y, assume D is binary almost everywhere, there is at least one time period, every cohort has strictly positive population mass, the cohort masses sum to one, each cohort's mass is split evenly across periods (a balanced panel law), on each cohort-period cell D is almost-everywhere equal to its own cell mean (cell-measurability of D), and the population per-cell residualized treatment panelDtilde agrees with the finite-panel residualized treatment Dtilde. Then the population second moment of the residualized-treatment witness — the FWL denominator ∫ Vtilde² dμ — equals the finite-cell Goodman-Bacon denominator VD of the induced finite panel.
Formal statement
Proof (Lean source)
On a probability space carrying cohort label G, period label T_rv, treatment D, and outcome Y, assume D is binary almost everywhere, there is at least one time period, every cohort has strictly positive population mass, the cohort masses sum to one, each cohort's mass is split evenly across periods (a balanced panel law), on each cohort-period cell D is almost-everywhere equal to its own cell mean (cell-measurability of D), and the population per-cell residualized treatment panelDtilde agrees with the finite-panel residualized treatment Dtilde. Then the finite-cell Goodman-Bacon denominator VD is strictly positive if and only if the population FWL denominator ∫ Vtilde² dμ is strictly positive.
Formal statement
Proof (Lean source)
On a probability space carrying cohort label G, period label T_rv, treatment D, and outcome Y, assume D is binary almost everywhere, there is at least one time period, every cohort has strictly positive population mass, the cohort masses sum to one, each cohort's mass is split evenly across periods (a balanced panel law), on each cohort-period cell D is almost-everywhere equal to its own cell mean (cell-measurability of D), and the population per-cell residualized treatment panelDtilde agrees with the finite-panel residualized treatment Dtilde. Then the population residualized regression coefficient of D on Y, controlling for the cohort/period additive class panelClass, equals the finite-cell Goodman-Bacon two-way-fixed-effects coefficient betaTWFE of the induced finite panel.