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.
inductive CompTag reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Three-valued tag for the type of an admissible 2x2 comparison: treated-versus-never, early-versus-late before late, and late-versus-early after early.
Definition (Lean source)
inductive CompTag | TN | EL | LE deriving DecidableEq
structure CohortPanel reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
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)
parameters
fields
Cohort population share `p_g`.
p :
𝒢 → ℝ
Adoption date `A_g ∈ 𝒯 ∪ {∞}`, encoded with `⊤ = ∞`.
Cohort-period factual outcome mean `Y_{gt}`.
Y :
𝒢 → Fin T → ℝ
The number of periods is positive.
T_pos :
0 < T
Cohort shares are strictly positive.
p_pos :
∀ g, 0 < p g
Cohort shares sum to one.
p_sum_one :
∑ g, p g = 1
def le reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition.AdoptionDate
Adoption-date predicate A_g ≤ t, i.e. cohort g has adopted by period t. The lift (t : WithTop (Fin T)) carries ⊤ = ∞ so that ∞ ≤ t is false, matching the LaTeX convention 1_{∞ ≤ t} = 0.
def lt reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition.AdoptionDate
Adoption-date predicate t < A_g, i.e. cohort g is untreated at period t.
def isFin reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition.AdoptionDate
A_g is finite, i.e. cohort g is eventually treated.
def isInf reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition.AdoptionDate
A_g = ∞, i.e. cohort g is never treated.
def D reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Treatment indicator D_{gt} = 1_{A_g ≤ t}, binary and absorbing. Marked noncomputable because the WithTop-order predicate is taken via classical decidability.
Definition (Lean source)
noncomputable def D (P : CohortPanel 𝒢 T) (g : 𝒢) (t : Fin T) : ℝ :=
if AdoptionDate.le (P.A g) t then 1 else 0
def barD reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Cohort treatment share \overline{D}_g := T⁻¹ ∑_t D_{gt}.
Definition (Lean source)
noncomputable def barD (P : CohortPanel 𝒢 T) (g : 𝒢) : ℝ :=
(T : ℝ)⁻¹ * ∑ t, D P g t
def pCohort reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Overall treatment share E[D] = ∑_g p_g \overline{D}_g.
Definition (Lean source)
def cohortWeights reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Cohort shares as unit weights for the shared weighted two-way panel module.
Definition (Lean source)
noncomputable def cohortWeights (P : CohortPanel 𝒢 T) :
WeightedTwoWayPanel.UnitWeights 𝒢 :=
⟨P.p, P.p_pos, P.p_sum_one⟩
def Dtilde reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Residualized treatment via the explicit double-demeaning formula \widetilde{D}_{gt} := D_{gt} − \overline{D}_g − E[D|T=t] + E[D].
Definition (Lean source)
noncomputable def Dtilde (P : CohortPanel 𝒢 T) (g : 𝒢) (t : Fin T) : ℝ :=
WeightedTwoWayPanel.ddot (cohortWeights P) (D P) g t
theorem Dtilde_eq reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
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
hypotheses
Proof (Lean source)
theorem Dtilde_eq (P : CohortPanel 𝒢 T) (g : 𝒢) (t : Fin T) :
Dtilde P g t =
D P g t - barD P g - (∑ g', P.p g' * D P g' t) + pCohort P := by
unfold Dtilde WeightedTwoWayPanel.ddot
rw [← barD_eq_unitMean P g, ← pCohort_eq_grandMean P]
unfold WeightedTwoWayPanel.timeMean cohortWeights
simp
def VD reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Residualized treatment variance V_D := ∑_{g,t} (p_g/T) \widetilde{D}_{gt}^2.
Definition (Lean source)
def betaTWFE reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Population TWFE coefficient (finite-cell form) from def:po-estimand-goodman-bacon-twfe. Defined unconditionally; positivity of the denominator is supplied at theorem-use time via hVD_pos.
Definition (Lean source)
noncomputable def betaTWFE (P : CohortPanel 𝒢 T) : ℝ :=
(∑ g, ∑ t, (P.p g / (T : ℝ)) * Dtilde P g t * P.Y g t) / VD P
def Ybar reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Window mean \overline{Y}_{g,S} := |S|⁻¹ ∑_{t ∈ S} Y_{gt}. Defined unconditionally; nonemptiness S.Nonempty is supplied as a hypothesis when used.
Definition (Lean source)
noncomputable def Ybar (P : CohortPanel 𝒢 T) (g : 𝒢) (S : Finset (Fin T)) : ℝ :=
(S.card : ℝ)⁻¹ * ∑ t ∈ S, P.Y g t
def S0_TN reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Treated-versus-never untreated window \mathcal{T}_g^0 = {t : t < A_g}.
Definition (Lean source)
noncomputable def S0_TN (P : CohortPanel 𝒢 T) (g : 𝒢) : Finset (Fin T) :=
Finset.univ.filter (fun t => AdoptionDate.lt (P.A g) t)
def S1_TN reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Treated-versus-never treated window \mathcal{T}_g^1 = {t : A_g ≤ t}.
Definition (Lean source)
noncomputable def S1_TN (P : CohortPanel 𝒢 T) (g : 𝒢) : Finset (Fin T) :=
Finset.univ.filter (fun t => AdoptionDate.le (P.A g) t)
def S0_EL reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Early-vs-late untreated window \mathcal{T}_{e\ell}^0 = {t : t < A_e}.
Definition (Lean source)
noncomputable def S0_EL (P : CohortPanel 𝒢 T) (e : 𝒢) : Finset (Fin T) :=
Finset.univ.filter (fun t => AdoptionDate.lt (P.A e) t)
def S1_EL reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Early-vs-late treated window \mathcal{T}_{e\ell}^1 = {t : A_e ≤ t < A_ℓ}.
Definition (Lean source)
noncomputable def S1_EL (P : CohortPanel 𝒢 T) (e ℓ : 𝒢) : Finset (Fin T) :=
Finset.univ.filter (fun t => AdoptionDate.le (P.A e) t ∧ AdoptionDate.lt (P.A ℓ) t)
def S0_LE reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Late-vs-early early-treated window \mathcal{T}_{\ell e}^0 = {t : A_e ≤ t < A_ℓ}.
Definition (Lean source)
def S1_LE reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Late-vs-early both-treated window \mathcal{T}_{\ell e}^1 = {t : A_ℓ ≤ t}.
Definition (Lean source)
noncomputable def S1_LE (P : CohortPanel 𝒢 T) (ℓ : 𝒢) : Finset (Fin T) :=
Finset.univ.filter (fun t => AdoptionDate.le (P.A ℓ) t)
def Δ_TN reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Treated-vs-never 2x2 DID contrast Δ^TN_{g,u}.
def Δ_EL reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Early-vs-late before late 2x2 DID contrast Δ^EL_{e,ℓ}.
def Δ_LE reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Late-vs-early after early 2x2 DID contrast Δ^LE_{ℓ,e}.
def lambdaTN reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Treated-vs-never raw weight λ^TN_{g,u} := p_g p_u \overline{D}_g (1−\overline{D}_g).
Definition (Lean source)
noncomputable def lambdaTN (P : CohortPanel 𝒢 T) (g u : 𝒢) : ℝ :=
P.p g * P.p u * (barD P g * (1 - barD P g))
def q reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Treated-treated timing-pair gap q_{eℓ} := \overline{D}_e − \overline{D}_ℓ.
Definition (Lean source)
def mu reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Splitting fraction μ_{eℓ} := (1−\overline{D}_e)/(1−q_{eℓ}).
Definition (Lean source)
def lambdaEL reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Early-vs-late raw weight λ^EL_{e,ℓ} := p_e p_ℓ q (1−q) μ.
Definition (Lean source)
noncomputable def lambdaEL (P : CohortPanel 𝒢 T) (e ℓ : 𝒢) : ℝ :=
P.p e * P.p ℓ * q P e ℓ * (1 - q P e ℓ) * mu P e ℓ
def lambdaLE reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Late-vs-early raw weight λ^LE_{ℓ,e} := p_e p_ℓ q (1−q) (1−μ).
Definition (Lean source)
noncomputable def lambdaLE (P : CohortPanel 𝒢 T) (e ℓ : 𝒢) : ℝ :=
P.p e * P.p ℓ * q P e ℓ * (1 - q P e ℓ) * (1 - mu P e ℓ)
def Lambda reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Aggregate raw-weight denominator Λ := ∑_{TN admissible} λ^TN + ∑_{e<ℓ<∞} (λ^EL + λ^LE).
Definition (Lean source)
noncomputable def Lambda (P : CohortPanel 𝒢 T) : ℝ :=
(∑ g, ∑ u, if AdoptionDate.isFin (P.A g) ∧ AdoptionDate.isInf (P.A u) then
lambdaTN P g u else 0)
+ (∑ e, ∑ ℓ, if P.A e < P.A ℓ ∧ AdoptionDate.isFin (P.A ℓ) then
lambdaEL P e ℓ + lambdaLE P e ℓ else 0)
def w_TN reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Normalized treated-vs-never weight w^TN_{g,u} := λ^TN_{g,u} / Λ.
Definition (Lean source)
def w_EL reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Normalized early-vs-late weight w^EL_{e,ℓ} := λ^EL_{e,ℓ} / Λ.
Definition (Lean source)
def w_LE reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Normalized late-vs-early weight w^LE_{ℓ,e} := λ^LE_{ℓ,e} / Λ.
Definition (Lean source)
def admissible reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Admissibility predicate for a tagged cohort pair (tag, g₁, g₂). For TN: g₁ eventually treated and g₂ never treated, both with positive shares. For EL/LE: A_{g₁} < A_{g₂} < ∞, both with positive shares.
Definition (Lean source)
def admissible (P : CohortPanel 𝒢 T) (k : CompTag × 𝒢 × 𝒢) : Prop :=
match k.1 with
| CompTag.TN =>
AdoptionDate.isFin (P.A k.2.1) ∧ AdoptionDate.isInf (P.A k.2.2)
∧ 0 < P.p k.2.1 ∧ 0 < P.p k.2.2
| CompTag.EL =>
P.A k.2.1 < P.A k.2.2 ∧ AdoptionDate.isFin (P.A k.2.2)
∧ 0 < P.p k.2.1 ∧ 0 < P.p k.2.2
| CompTag.LE =>
P.A k.2.1 < P.A k.2.2 ∧ AdoptionDate.isFin (P.A k.2.2)
∧ 0 < P.p k.2.1 ∧ 0 < P.p k.2.2
def 𝒦 reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Comparison index set 𝒦 P : Finset (CompTag × 𝒢 × 𝒢), the set of all admissible 2x2 comparisons.
Definition (Lean source)
noncomputable def 𝒦 (P : CohortPanel 𝒢 T) : Finset (CompTag × 𝒢 × 𝒢) :=
(Finset.univ : Finset (CompTag × 𝒢 × 𝒢)).filter (fun k => admissible P k)
def weight reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Unified normalized weight on the full index CompTag × 𝒢 × 𝒢: returns the matching w_TN/w_EL/w_LE on admissible triples and 0 otherwise.
Definition (Lean source)
noncomputable def weight (P : CohortPanel 𝒢 T) (k : CompTag × 𝒢 × 𝒢) : ℝ :=
if admissible P k then
match k.1 with
| CompTag.TN => w_TN P k.2.1 k.2.2
| CompTag.EL => w_EL P k.2.1 k.2.2
| CompTag.LE => w_LE P k.2.1 k.2.2
else 0
def contrast reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Unified 2x2 contrast on the full index CompTag × 𝒢 × 𝒢: returns the matching Δ_TN/Δ_EL/Δ_LE on admissible triples and 0 otherwise.
Definition (Lean source)
noncomputable def contrast (P : CohortPanel 𝒢 T) (k : CompTag × 𝒢 × 𝒢) : ℝ :=
if admissible P k then
match k.1 with
| CompTag.TN => Δ_TN P k.2.1 k.2.2
| CompTag.EL => Δ_EL P k.2.1 k.2.2
| CompTag.LE => Δ_LE P k.2.1 k.2.2
else 0
def lambdaWeight reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Unified raw weight on the full index CompTag × 𝒢 × 𝒢: returns the matching λ_TN/λ_EL/λ_LE on admissible triples and 0 otherwise.
Definition (Lean source)
noncomputable def lambdaWeight (P : CohortPanel 𝒢 T) (k : CompTag × 𝒢 × 𝒢) : ℝ :=
if admissible P k then
match k.1 with
| CompTag.TN => lambdaTN P k.2.1 k.2.2
| CompTag.EL => lambdaEL P k.2.1 k.2.2
| CompTag.LE => lambdaLE P k.2.1 k.2.2
else 0
4 supporting declarations (lemmas, instances)
-
instDecidableEqCompTaginductiveinductive CompTag | TN | EL | LE deriving DecidableEq -
barD_eq_unitMeantheorem — Goodman-Bacon's cohort treatment share is the shared unit mean.Proof (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.hypothesesP :CohortPanel 𝒢 TconclusionpCohort 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.
def Ybar0 reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Window mean of a potential-outcome map Y* : 𝒢 → Fin T → ℝ, Ȳ_{g(*),S} := |S|⁻¹ ∑_{t ∈ S} Y*_{gt}. Defined unconditionally; nonemptiness of S is supplied at theorem-use time.
def ATT_window reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Window-specific ATT in the two-state Goodman-Bacon causal layer: ATT_{g,S} := |S|⁻¹ ∑_{t ∈ S} (Y_{gt}(A_g) − Y_{gt}(∞)), parameterized by potential-outcome maps Y0 = Y(∞) and Y1 = Y(A_g).
Definition (Lean source)
noncomputable def ATT_window (Y0 Y1 : 𝒢 → Fin T → ℝ) (g : 𝒢)
(S : Finset (Fin T)) : ℝ :=
(S.card : ℝ)⁻¹ * ∑ t ∈ S, (Y1 g t - Y0 g t)
structure CausalAssumptions reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
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)
parameters
P :
CohortPanel 𝒢 T
Y0 Y1 :
𝒢 → Fin T → ℝ
fields
Consistency on treated cells: when `A_g ≤ t`, the factual outcome
equals the post-adoption potential outcome.
consistencyTreated :
∀ g t
if
AdoptionDate.le (P.A g) t
then
P.Y g t = Y1 g t
Consistency on untreated cells: when `t < A_g`, the factual outcome
equals the never-treated potential outcome.
consistencyUntreated :
∀ g t
if
AdoptionDate.lt (P.A g) t
then
P.Y g t = Y0 g t
No anticipation: pre-adoption potential outcomes coincide.
noAnticipation :
∀ g t
if
AdoptionDate.lt (P.A g) t
then
Y1 g t = Y0 g t
Pairwise untreated parallel trends for treated-vs-never (TN).
parallelTrends_TN :
Pairwise untreated parallel trends for early-vs-late before late (EL).
parallelTrends_EL :
Pairwise untreated parallel trends for late-vs-early after early (LE).
theorem Δ_TN_eq_ATT reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
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
hypotheses
P :
CohortPanel 𝒢 T
Y0 Y1 :
𝒢 → Fin T → ℝ
hA :
CausalAssumptions P Y0 Y1
g u :
𝒢
h_g_fin :
AdoptionDate.isFin (P.A g)
h_u_inf :
AdoptionDate.isInf (P.A u)
conclusion
Proof (Lean source)
theorem Δ_TN_eq_ATT (P : CohortPanel 𝒢 T) (Y0 Y1 : 𝒢 → Fin T → ℝ)
(hA : CausalAssumptions P Y0 Y1) (g u : 𝒢)
(h_g_fin : AdoptionDate.isFin (P.A g))
(h_u_inf : AdoptionDate.isInf (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 [S1_TN, mem_filter] 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 _ _ => CausalAssumptions.AdoptionDate.lt_of_isInf h_u_inf)
have h_u0 := CausalAssumptions.Ybar_eq_Ybar0_of_inf hA.consistencyUntreated
(S0_TN P g) (fun _ _ => CausalAssumptions.AdoptionDate.lt_of_isInf 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
theorem Δ_EL_eq_ATT reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
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
hypotheses
P :
CohortPanel 𝒢 T
Y0 Y1 :
𝒢 → Fin T → ℝ
hA :
CausalAssumptions P Y0 Y1
e ℓ :
𝒢
h_lt :
P.A e < P.A ℓ
h_ℓ_fin :
AdoptionDate.isFin (P.A ℓ)
conclusion
Proof (Lean source)
theorem Δ_EL_eq_ATT (P : CohortPanel 𝒢 T) (Y0 Y1 : 𝒢 → Fin T → ℝ)
(hA : CausalAssumptions P Y0 Y1) (e ℓ : 𝒢)
(h_lt : P.A e < P.A ℓ) (h_ℓ_fin : AdoptionDate.isFin (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 :
AdoptionDate.le (P.A e) t ∧ AdoptionDate.lt (P.A ℓ) t := by
simpa [S1_EL, mem_filter] 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
theorem Δ_LE_eq_bad_comparison reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
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
hypotheses
P :
CohortPanel 𝒢 T
Y0 Y1 :
𝒢 → Fin T → ℝ
hA :
CausalAssumptions P Y0 Y1
e ℓ :
𝒢
h_lt :
P.A e < P.A ℓ
h_ℓ_fin :
AdoptionDate.isFin (P.A ℓ)
conclusion
Δ_LE P e ℓ
= ATT_window Y0 Y1 ℓ (S1_LE P ℓ)
Proof (Lean source)
theorem Δ_LE_eq_bad_comparison (P : CohortPanel 𝒢 T) (Y0 Y1 : 𝒢 → Fin T → ℝ)
(hA : CausalAssumptions P Y0 Y1) (e ℓ : 𝒢)
(h_lt : P.A e < P.A ℓ) (h_ℓ_fin : AdoptionDate.isFin (P.A ℓ)) :
Δ_LE P e ℓ
= ATT_window Y0 Y1 ℓ (S1_LE P ℓ)
- (ATT_window Y0 Y1 e (S1_LE P ℓ)
- ATT_window Y0 Y1 e (S0_LE P e ℓ)) := by
classical
have h_l1 :
Ybar P ℓ (S1_LE P ℓ) =
Ybar0 Y0 ℓ (S1_LE P ℓ) + ATT_window Y0 Y1 ℓ (S1_LE P ℓ) := by
exact CausalAssumptions.Ybar_eq_Ybar0_add_ATT_of_treated hA.consistencyTreated ℓ (S1_LE P ℓ) (by
intro t ht
simpa [S1_LE, mem_filter] using ht)
have h_l0 := CausalAssumptions.Ybar_eq_Ybar0_late_on_S0_LE hA.consistencyUntreated e ℓ
have h_e0 :
Ybar P e (S0_LE P e ℓ) =
Ybar0 Y0 e (S0_LE P e ℓ) + ATT_window Y0 Y1 e (S0_LE P e ℓ) := by
exact CausalAssumptions.Ybar_eq_Ybar0_add_ATT_of_treated hA.consistencyTreated e
(S0_LE P e ℓ) (by
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 htmem.1)
have h_e1 :
Ybar P e (S1_LE P ℓ) =
Ybar0 Y0 e (S1_LE P ℓ) + ATT_window Y0 Y1 e (S1_LE P ℓ) := by
exact CausalAssumptions.Ybar_eq_Ybar0_add_ATT_of_treated hA.consistencyTreated e (S1_LE P ℓ) (by
intro t ht
have hle : AdoptionDate.le (P.A ℓ) t := by
simpa [S1_LE, mem_filter] using ht
exact le_of_lt (lt_of_lt_of_le h_lt hle))
have hPT := hA.parallelTrends_LE e ℓ h_lt h_ℓ_fin
unfold Δ_LE
rw [h_l1, h_l0, h_e1, h_e0]
linarith
9 supporting declarations (lemmas, instances)
-
not_le_of_lttheorem — Helper: AdoptionDate.lt (P.A g) t rules out AdoptionDate.le (P.A g) t.Proof (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.hypotheseshConsistency :∀ 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.hypotheseshConsistency :∀ 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.hypotheseshConsistency :∀ 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.hypotheseshConsistency :∀ 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_ℓ.hypotheseshConsistency :∀ 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_ℓ.hypotheseshConsistency :∀ 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.hypotheseshConsistency :∀ 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.
theorem weights_nonneg reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
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)
theorem weights_nonneg (P : CohortPanel 𝒢 T) (k : CompTag × 𝒢 × 𝒢) :
0 ≤ lambdaWeight P k := by
classical
unfold lambdaWeight
have hTpos : 0 < (T : ℝ) := by exact_mod_cast P.T_pos
have hTnonneg : 0 ≤ (T : ℝ) := le_of_lt hTpos
have hTne : (T : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt P.T_pos)
have hbar_nonneg : ∀ g : 𝒢, 0 ≤ barD P g := by
intro g
unfold barD
have hsum_nonneg : 0 ≤ ∑ t : Fin T, D P g t := by
refine Finset.sum_nonneg' ?_
intro t
by_cases hD : AdoptionDate.le (P.A g) t
· simp [D, hD]
· simp [D, hD]
simpa using (mul_nonneg (inv_nonneg.mpr hTnonneg) hsum_nonneg)
have hbar_le_one : ∀ g : 𝒢, barD P g ≤ 1 := by
intro g
unfold barD
have hsum_le : ∑ t : Fin T, D P g t ≤ (T : ℝ) := by
have hsum_le' : (∑ t : Fin T, D P g t) ≤ (∑ t : Fin T, (1 : ℝ)) := by
refine Finset.sum_le_sum ?_
intro t ht
by_cases hD : AdoptionDate.le (P.A g) t
· simp [D, hD]
· simp [D, hD]
simpa using hsum_le'
have hsum_le'' : (∑ t, D P g t) ≤ (T : ℝ) := by simpa using hsum_le
have htmp : (T : ℝ)⁻¹ * (∑ t, D P g t) ≤ (T : ℝ)⁻¹ * (T : ℝ) :=
mul_le_mul_of_nonneg_left hsum_le'' (inv_nonneg.mpr hTnonneg)
simpa [barD, inv_mul_cancel₀ hTne] using htmp
by_cases h : admissible P k
· simp only [h, if_true]
rcases k with ⟨tag, g, u⟩
cases tag with
| TN =>
rcases h with ⟨_, _, hpg, hpu⟩
have hmul : 0 ≤ (P.p g * P.p u) * (barD P g * (1 - barD P g)) := by
exact mul_nonneg (mul_nonneg (le_of_lt hpg) (le_of_lt hpu))
(mul_nonneg (hbar_nonneg g) (sub_nonneg.mpr (hbar_le_one g)))
simpa [lambdaTN, mul_assoc, mul_left_comm, mul_comm] using hmul
| EL =>
rcases h with ⟨hlt, _, hpg, hpu⟩
have hbar_mono : barD P u ≤ barD P g := by
unfold barD
have hsum_le : (∑ t : Fin T, D P u t) ≤ (∑ t : Fin T, D P g t) := by
refine Finset.sum_le_sum ?_
intro t ht
by_cases htu : AdoptionDate.le (P.A u) t
· have htg : AdoptionDate.le (P.A g) t :=
le_of_lt (lt_of_lt_of_le hlt htu)
simp [D, htu, htg]
· by_cases htg : AdoptionDate.le (P.A g) t
· simp [D, htu, htg]
· simp [D, htu, htg]
have hsum_le' : (∑ t : Fin T, D P u t) ≤ (∑ t : Fin T, D P g t) := by
simpa using hsum_le
exact mul_le_mul_of_nonneg_left hsum_le' (inv_nonneg.mpr hTnonneg)
have hq_nonneg : 0 ≤ q P g u := by
unfold q
exact sub_nonneg.mpr hbar_mono
have hq_le_barD : q P g u ≤ barD P g := by
unfold q
nlinarith [hbar_mono, hbar_nonneg u]
have hq_le_one : q P g u ≤ 1 := le_trans hq_le_barD (hbar_le_one g)
have h1mq_nonneg : 0 ≤ 1 - q P g u := sub_nonneg.mpr hq_le_one
have hmu_nonneg : 0 ≤ mu P g u := by
unfold mu
exact div_nonneg (sub_nonneg.mpr (hbar_le_one g)) h1mq_nonneg
have hnum_le_den : 1 - barD P g ≤ 1 - q P g u := by
have hlu_nonneg : 0 ≤ barD P u := hbar_nonneg u
unfold q
linarith
have hmu_le_one : mu P g u ≤ 1 := by
by_cases hden : 1 - q P g u = 0
· have hqeq : q P g u = 1 := by linarith
simp [mu, hqeq]
· have hden_pos : 0 < 1 - q P g u :=
lt_of_le_of_ne h1mq_nonneg (Ne.symm hden)
have hdiv : (1 - barD P g) / (1 - q P g u) ≤ 1 :=
(div_le_one₀ hden_pos).2 hnum_le_den
simpa [mu] using hdiv
have h1m_nonneg : 0 ≤ 1 - mu P g u := sub_nonneg.mpr hmu_le_one
have hmul : 0 ≤ P.p g * P.p u * (q P g u * (1 - q P g u) * mu P g u) := by
have hmul1 : 0 ≤ P.p g * P.p u := mul_nonneg (le_of_lt hpg) (le_of_lt hpu)
have hmul2 : 0 ≤ q P g u * (1 - q P g u) := mul_nonneg hq_nonneg h1mq_nonneg
have hmul3 : 0 ≤ q P g u * (1 - q P g u) * mu P g u := mul_nonneg hmul2 hmu_nonneg
exact mul_nonneg hmul1 hmul3
simpa [lambdaEL, mul_assoc, mul_left_comm, mul_comm] using hmul
| LE =>
rcases h with ⟨hlt, _, hpg, hpu⟩
have hbar_mono : barD P u ≤ barD P g := by
unfold barD
have hsum_le : (∑ t : Fin T, D P u t) ≤ (∑ t : Fin T, D P g t) := by
refine Finset.sum_le_sum ?_
intro t ht
by_cases htu : AdoptionDate.le (P.A u) t
· have htg : AdoptionDate.le (P.A g) t :=
le_of_lt (lt_of_lt_of_le hlt htu)
simp [D, htu, htg]
· by_cases htg : AdoptionDate.le (P.A g) t
· simp [D, htu, htg]
· simp [D, htu, htg]
have hsum_le' : (∑ t : Fin T, D P u t) ≤ (∑ t : Fin T, D P g t) := by
simpa using hsum_le
exact mul_le_mul_of_nonneg_left hsum_le' (inv_nonneg.mpr hTnonneg)
have hq_nonneg : 0 ≤ q P g u := by
unfold q
exact sub_nonneg.mpr hbar_mono
have hq_le_barD : q P g u ≤ barD P g := by
unfold q
nlinarith [hbar_mono, hbar_nonneg u]
have hq_le_one : q P g u ≤ 1 := le_trans hq_le_barD (hbar_le_one g)
have h1mq_nonneg : 0 ≤ 1 - q P g u := sub_nonneg.mpr hq_le_one
have hmu_nonneg : 0 ≤ mu P g u := by
unfold mu
exact div_nonneg (sub_nonneg.mpr (hbar_le_one g)) h1mq_nonneg
have hnum_le_den : 1 - barD P g ≤ 1 - q P g u := by
have hlu_nonneg : 0 ≤ barD P u := hbar_nonneg u
unfold q
linarith
have hmu_le_one : mu P g u ≤ 1 := by
by_cases hden : 1 - q P g u = 0
· have hqeq : q P g u = 1 := by linarith
simp [mu, hqeq]
· have hden_pos : 0 < 1 - q P g u :=
lt_of_le_of_ne h1mq_nonneg (Ne.symm hden)
have hdiv : (1 - barD P g) / (1 - q P g u) ≤ 1 := by
exact (div_le_one₀ hden_pos).2 hnum_le_den
simpa [mu] using hdiv
have h1m_nonneg : 0 ≤ 1 - mu P g u := sub_nonneg.mpr hmu_le_one
have hmul : 0 ≤ P.p g * P.p u * (q P g u * (1 - q P g u) * (1 - mu P g u)) := by
have hmul1 : 0 ≤ P.p g * P.p u := mul_nonneg (le_of_lt hpg) (le_of_lt hpu)
have hmul2 : 0 ≤ q P g u * (1 - q P g u) := mul_nonneg hq_nonneg h1mq_nonneg
have hmul3 : 0 ≤ q P g u * (1 - q P g u) * (1 - mu P g u) := mul_nonneg hmul2 h1m_nonneg
exact mul_nonneg hmul1 hmul3
simpa [lambdaLE, mul_assoc, mul_left_comm, mul_comm] using hmul
· simp [h]
theorem weights_sum_one reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
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 weights_sum_one (P : CohortPanel 𝒢 T) (hVD_pos : 0 < VD P) :
∑ k ∈ 𝒦 P, weight P k = 1 := by
classical
have hL_ne : Lambda P ≠ 0 := by
rw [raw_weight_sum_eq_VD P]
exact ne_of_gt hVD_pos
have hsum_lambda : ∑ k ∈ 𝒦 P, lambdaWeight P k = Lambda P := by
exact sum_lambdaWeight_eq_Lambda P
calc
∑ k ∈ 𝒦 P, weight P k = ∑ k ∈ 𝒦 P, lambdaWeight P k / Lambda P := by
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']
_ = (∑ k ∈ 𝒦 P, lambdaWeight P k) / Lambda P := by
simp [div_eq_mul_inv, Finset.mul_sum, mul_comm]
_ = Lambda P / Lambda P := by rw [hsum_lambda]
_ = 1 := by exact div_self hL_ne
theorem twfe_eq_weighted_avg reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
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)
theorem twfe_eq_weighted_avg (P : CohortPanel 𝒢 T) :
betaTWFE P = ∑ k ∈ 𝒦 P, weight P k * contrast P k :=
twfe_eq_weighted_avg_core P
11 supporting declarations (lemmas, instances)
-
barD_eq_zero_of_isInflemma — A never-treated cohort has zero average treatment over the panel.Proof (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.hypothesesP :CohortPanel 𝒢 Te ℓ :𝒢Proof (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.hypothesesP :CohortPanel 𝒢 TconclusionLambda 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.Proof (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.hypothesesconclusion(∑ 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.hypothesesP :CohortPanel 𝒢 Tconclusion(∑ 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.Proof (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.Proof (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.Proof (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.
def contrastCausal reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
The causal 2x2 contrast on the full index CompTag × 𝒢 × 𝒢: on an admissible comparison it returns the potential-outcome window contrast identified by the Layer C corollaries — ATT_window for TN/EL and the bad-comparison adjustment for LE — and 0 otherwise. This is the causal counterpart of the algebraic contrast.
Definition (Lean source)
noncomputable def contrastCausal (P : CohortPanel 𝒢 T) (Y0 Y1 : 𝒢 → Fin T → ℝ)
(k : CompTag × 𝒢 × 𝒢) : ℝ :=
if admissible P k then
match k.1 with
| CompTag.TN => ATT_window Y0 Y1 k.2.1 (S1_TN P k.2.1)
| CompTag.EL => ATT_window Y0 Y1 k.2.1 (S1_EL P k.2.1 k.2.2)
| CompTag.LE =>
ATT_window Y0 Y1 k.2.2 (S1_LE P k.2.2)
- (ATT_window Y0 Y1 k.2.1 (S1_LE P k.2.2)
- ATT_window Y0 Y1 k.2.1 (S0_LE P k.2.1 k.2.2))
else 0
theorem twfe_po_decomposition reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
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
hypotheses
conclusion
betaTWFE P = ∑ k ∈ 𝒦 P, weight P k * contrastCausal P Y0 Y1 k
Proof (Lean source)
theorem twfe_po_decomposition (P : CohortPanel 𝒢 T) (Y0 Y1 : 𝒢 → Fin T → ℝ)
(hA : CausalAssumptions P Y0 Y1) :
betaTWFE P = ∑ k ∈ 𝒦 P, weight P k * contrastCausal P Y0 Y1 k := by
rw [twfe_eq_weighted_avg_core P]
refine Finset.sum_congr rfl ?_
intro k hk
have hk' : admissible P k := by simpa [𝒦] using hk
rw [contrast_eq_contrastCausal P Y0 Y1 hA hk']
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.hypothesesP :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.
def centeredD reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Cohort-demeaned treatment path D_{gt} − \overline D_g.
Definition (Lean source)
def vdPairContribution reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Ordered-pair contribution in the pairwise representation of V_D.
Definition (Lean source)
noncomputable def vdPairContribution (P : CohortPanel 𝒢 T) (g u : 𝒢) : ℝ :=
(P.p g * P.p u / (2 * (T : ℝ))) *
∑ t, (centeredD P g t - centeredD P u t)^2
def numPairContribution reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Ordered-pair contribution in the pairwise representation of the TWFE numerator. As for vdPairContribution, the two orders of each cohort pair are combined by the Goodman-Bacon-specific window lemmas below.
Definition (Lean source)
noncomputable def numPairContribution (P : CohortPanel 𝒢 T) (g u : 𝒢) : ℝ :=
(P.p g * P.p u / (2 * (T : ℝ))) *
∑ t, (centeredD P g t - centeredD P u t) * (P.Y g t - P.Y u t)
lemma VD_eq_pairwise_centeredD reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
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)
lemma VD_eq_pairwise_centeredD (P : CohortPanel 𝒢 T) :
VD P = ∑ g, ∑ u, vdPairContribution P g u := by
classical
calc
VD P = (T : ℝ)⁻¹ * ∑ t, ∑ g, P.p g * (Dtilde P g t)^2 := by
unfold VD
exact sum_weight_over_T_commute P (fun g t => (Dtilde P g t)^2)
_ = (T : ℝ)⁻¹ * ∑ t, ∑ g, P.p g *
(centeredD P g t - ∑ h, P.p h * centeredD P h t)^2 := 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]
_ = (T : ℝ)⁻¹ * ∑ t,
((1 / 2) * ∑ g, ∑ u, P.p g * P.p u *
(centeredD P g t - centeredD P u t)^2) := by
congr 1
refine Finset.sum_congr rfl ?_
intro t _ht
exact weighted_center_var (fun g => P.p g)
(fun g => centeredD P g t) P.p_sum_one (by norm_num)
_ = ∑ g, ∑ u, vdPairContribution P g u := by
unfold vdPairContribution
exact pairwise_sum_normalize P
(fun g u t => (centeredD P g t - centeredD P u t)^2)
lemma TN_pair_contribution_eq_lambda_delta reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
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
hypotheses
conclusion
Proof (Lean source)
lemma TN_pair_contribution_eq_lambda_delta
(P : CohortPanel 𝒢 T) {g u : 𝒢}
(hg : AdoptionDate.isFin (P.A g)) (hu : AdoptionDate.isInf (P.A u)) :
numPairContribution P g u + numPairContribution P u g =
lambdaTN P g u * Δ_TN P g u := by
rw [numPairContribution_add_swap]
have hTne : (T : ℝ) ≠ 0 := by
exact_mod_cast (ne_of_gt P.T_pos)
have hcov := TN_time_cov_eq_lambda_delta_core P hg hu
calc
(P.p g * P.p u / (T : ℝ)) *
∑ t, (centeredD P g t - centeredD P u t) * (P.Y g t - P.Y u t) =
P.p g * P.p u *
((T : ℝ)⁻¹ * ∑ t,
(centeredD P g t - centeredD P u t) * (P.Y g t - P.Y u t)) := by
field_simp [hTne]
_ = lambdaTN P g u * Δ_TN P g u := by
rw [hcov]
unfold lambdaTN
ring
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.hypothesesP :CohortPanel 𝒢 Tf :𝒢 → Fin T → ℝconclusion(∑ 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.hypothesesP :CohortPanel 𝒢 Tf :𝒢 → 𝒢 → Fin T → ℝconclusion(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.hypothesesconclusionD 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.Proof (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.hypothesesconclusion(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.hypothesesP :CohortPanel 𝒢 Tconclusion(∑ 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.hypothesesconclusionnumPairContribution 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.
theorem bridge_Dtilde_sq_eq_VD reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
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
hypotheses
μ :
D Y :
Ω → ℝ
G :
Ω → 𝒢
T_rv :
Ω → Fin T
G_meas :
T_meas :
Measurable T_rv
D_meas :
D_binary :
∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1
B_balanced :
IsBalancedPanelLaw μ G T_rv
hT_pos :
0 < T
hp_pos :
∀ g, 0 < cohortMass μ G g
hp_sum :
∑ g, cohortMass μ G g = 1
hLaw :
∀ g t, cellMass μ G T_rv g t = cohortMass μ G g / (T : ℝ)
hD_cell :
∀ g t,
∀ᵐ ω ∂μ.restrict {ω' | G ω' = g ∧ T_rv ω' = t},
D ω
= (∫ ω', D ω' * indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω' ∂μ) / cellMass μ G T_rv g t
hDtilde_eq :
conclusion
(∫ ω, (residWitnessD_panel μ D G T_rv G_meas T_meas D_meas D_binary B_balanced).Vtilde ω * (residWitnessD_panel μ D G T_rv G_meas T_meas D_meas D_binary B_balanced).Vtilde ω ∂μ)
Proof (Lean source)
theorem bridge_Dtilde_sq_eq_VD
(μ : Measure Ω) [IsProbabilityMeasure μ]
(D Y : Ω → ℝ) (G : Ω → 𝒢) (T_rv : Ω → Fin T)
(A : 𝒢 → WithTop (Fin T))
(G_meas : Measurable G) (T_meas : Measurable T_rv)
(D_meas : Measurable D)
(D_binary : ∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1)
(B_balanced : IsBalancedPanelLaw μ G T_rv)
(hT_pos : 0 < T)
(hp_pos : ∀ g, 0 < cohortMass μ G g)
(hp_sum : ∑ g, cohortMass μ G g = 1)
(hLaw : ∀ g t,
cellMass μ G T_rv g t = cohortMass μ G g / (T : ℝ))
(hD_cell : ∀ g t, ∀ᵐ ω ∂μ.restrict {ω' | G ω' = g ∧ T_rv ω' = t},
D ω = (∫ ω', D ω' * indicator {ω' | G ω' = g ∧ T_rv ω' = t}
(fun _ => (1 : ℝ)) ω' ∂μ) / cellMass μ G T_rv g t)
(hDtilde_eq : ∀ g t,
panelDtilde μ D G T_rv g t =
Dtilde (panelOf μ Y G T_rv A hT_pos hp_pos hp_sum) g t) :
(∫ ω, (residWitnessD_panel μ D G T_rv G_meas T_meas D_meas D_binary
B_balanced).Vtilde ω
* (residWitnessD_panel μ D G T_rv G_meas T_meas D_meas D_binary
B_balanced).Vtilde ω ∂μ)
= VD (panelOf μ Y G T_rv A hT_pos hp_pos hp_sum) := by
let wD := residWitnessD_panel μ D G T_rv G_meas T_meas D_meas D_binary
B_balanced
let P := panelOf μ Y G T_rv A hT_pos hp_pos hp_sum
have hDen_sum :
∫ ω, wD.Vtilde ω * wD.Vtilde ω ∂μ =
∑ g, ∑ t, cellMass μ G T_rv g t
* (panelDtilde μ D G T_rv g t)^2 := by
have hF_int : Integrable (fun ω => wD.Vtilde ω * wD.Vtilde ω) μ :=
wD.Vtilde_memLp.integrable_mul wD.Vtilde_memLp
calc
∫ ω, wD.Vtilde ω * wD.Vtilde ω ∂μ =
∑ g, ∑ t, ∫ ω, (wD.Vtilde ω * wD.Vtilde ω)
* indicator {ω' | G ω' = g ∧ T_rv ω' = t}
(fun _ => (1 : ℝ)) ω ∂μ :=
integral_eq_sum_panel_cell μ (fun ω => wD.Vtilde ω * wD.Vtilde ω)
G T_rv G_meas T_meas hF_int
_ = ∑ g, ∑ t, cellMass μ G T_rv g t
* (panelDtilde μ D G T_rv g t)^2 := by
refine Finset.sum_congr rfl (fun g _ => ?_)
refine Finset.sum_congr rfl (fun t _ => ?_)
simpa [wD, residWitnessD_panel, mul_assoc] using
denom_per_cell_panel μ D G T_rv G_meas T_meas g t (hD_cell g t)
calc
∫ ω, (residWitnessD_panel μ D G T_rv G_meas T_meas D_meas D_binary
B_balanced).Vtilde ω
* (residWitnessD_panel μ D G T_rv G_meas T_meas D_meas D_binary
B_balanced).Vtilde ω ∂μ
= ∫ ω, wD.Vtilde ω * wD.Vtilde ω ∂μ := by rfl
_ = ∑ g, ∑ t, cellMass μ G T_rv g t
* (panelDtilde μ D G T_rv g t)^2 := hDen_sum
_ = VD P := by
simp [P, panelOf, VD, hLaw, hDtilde_eq]
theorem bridge_VD_pos_iff_Dtilde_sq_pos reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
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
hypotheses
μ :
D Y :
Ω → ℝ
G :
Ω → 𝒢
T_rv :
Ω → Fin T
G_meas :
T_meas :
Measurable T_rv
D_meas :
D_binary :
∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1
B_balanced :
IsBalancedPanelLaw μ G T_rv
hT_pos :
0 < T
hp_pos :
∀ g, 0 < cohortMass μ G g
hp_sum :
∑ g, cohortMass μ G g = 1
hLaw :
∀ g t, cellMass μ G T_rv g t = cohortMass μ G g / (T : ℝ)
hD_cell :
∀ g t,
∀ᵐ ω ∂μ.restrict {ω' | G ω' = g ∧ T_rv ω' = t},
D ω
= (∫ ω', D ω' * indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω' ∂μ) / cellMass μ G T_rv g t
hDtilde_eq :
conclusion
↔ 0 < ∫ ω, (residWitnessD_panel μ D G T_rv G_meas T_meas D_meas D_binary B_balanced).Vtilde ω * (residWitnessD_panel μ D G T_rv G_meas T_meas D_meas D_binary B_balanced).Vtilde ω ∂μ
Proof (Lean source)
theorem bridge_VD_pos_iff_Dtilde_sq_pos
(μ : Measure Ω) [IsProbabilityMeasure μ]
(D Y : Ω → ℝ) (G : Ω → 𝒢) (T_rv : Ω → Fin T)
(A : 𝒢 → WithTop (Fin T))
(G_meas : Measurable G) (T_meas : Measurable T_rv)
(D_meas : Measurable D)
(D_binary : ∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1)
(B_balanced : IsBalancedPanelLaw μ G T_rv)
(hT_pos : 0 < T)
(hp_pos : ∀ g, 0 < cohortMass μ G g)
(hp_sum : ∑ g, cohortMass μ G g = 1)
(hLaw : ∀ g t,
cellMass μ G T_rv g t = cohortMass μ G g / (T : ℝ))
(hD_cell : ∀ g t, ∀ᵐ ω ∂μ.restrict {ω' | G ω' = g ∧ T_rv ω' = t},
D ω = (∫ ω', D ω' * indicator {ω' | G ω' = g ∧ T_rv ω' = t}
(fun _ => (1 : ℝ)) ω' ∂μ) / cellMass μ G T_rv g t)
(hDtilde_eq : ∀ g t,
panelDtilde μ D G T_rv g t =
Dtilde (panelOf μ Y G T_rv A hT_pos hp_pos hp_sum) g t) :
0 < VD (panelOf μ Y G T_rv A hT_pos hp_pos hp_sum) ↔
0 < ∫ ω, (residWitnessD_panel μ D G T_rv G_meas T_meas D_meas D_binary
B_balanced).Vtilde ω
* (residWitnessD_panel μ D G T_rv G_meas T_meas D_meas D_binary
B_balanced).Vtilde ω ∂μ := by
rw [bridge_Dtilde_sq_eq_VD μ D Y G T_rv A G_meas T_meas D_meas D_binary
B_balanced hT_pos hp_pos hp_sum hLaw hD_cell hDtilde_eq]
theorem bridge_finite_residualized_eq_twfe reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
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.
Formal statement
hypotheses
μ :
D Y :
Ω → ℝ
G :
Ω → 𝒢
T_rv :
Ω → Fin T
G_meas :
T_meas :
Measurable T_rv
D_meas :
D_binary :
∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1
Y_memLp :
MemLp Y 2 μ
B_balanced :
IsBalancedPanelLaw μ G T_rv
hT_pos :
0 < T
hp_pos :
∀ g, 0 < cohortMass μ G g
hp_sum :
∑ g, cohortMass μ G g = 1
hLaw :
∀ g t, cellMass μ G T_rv g t = cohortMass μ G g / (T : ℝ)
hD_cell :
∀ g t,
∀ᵐ ω ∂μ.restrict {ω' | G ω' = g ∧ T_rv ω' = t},
D ω
= (∫ ω', D ω' * indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω' ∂μ) / cellMass μ G T_rv g t
hDtilde_eq :
conclusion
residualizedCoefficient μ (panelClass μ G T_rv G_meas T_meas) (residWitnessY_panel μ Y G T_rv G_meas T_meas Y_memLp B_balanced) (residWitnessD_panel μ D G T_rv G_meas T_meas D_meas D_binary B_balanced)
= betaTWFE (panelOf μ Y G T_rv A hT_pos hp_pos hp_sum)
Proof (Lean source)
theorem bridge_finite_residualized_eq_twfe
(μ : Measure Ω) [IsProbabilityMeasure μ]
(D Y : Ω → ℝ) (G : Ω → 𝒢) (T_rv : Ω → Fin T)
(A : 𝒢 → WithTop (Fin T))
(G_meas : Measurable G) (T_meas : Measurable T_rv)
(D_meas : Measurable D)
(D_binary : ∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1)
(Y_memLp : MemLp Y 2 μ)
(B_balanced : IsBalancedPanelLaw μ G T_rv)
(hT_pos : 0 < T)
(hp_pos : ∀ g, 0 < cohortMass μ G g)
(hp_sum : ∑ g, cohortMass μ G g = 1)
(hLaw : ∀ g t,
cellMass μ G T_rv g t = cohortMass μ G g / (T : ℝ))
(hD_cell : ∀ g t, ∀ᵐ ω ∂μ.restrict {ω' | G ω' = g ∧ T_rv ω' = t},
D ω = (∫ ω', D ω' * indicator {ω' | G ω' = g ∧ T_rv ω' = t}
(fun _ => (1 : ℝ)) ω' ∂μ) / cellMass μ G T_rv g t)
(hDtilde_eq : ∀ g t,
panelDtilde μ D G T_rv g t =
Dtilde (panelOf μ Y G T_rv A hT_pos hp_pos hp_sum) g t) :
residualizedCoefficient μ (panelClass μ G T_rv G_meas T_meas)
(residWitnessY_panel μ Y G T_rv G_meas T_meas Y_memLp B_balanced)
(residWitnessD_panel μ D G T_rv G_meas T_meas D_meas D_binary
B_balanced)
= betaTWFE (panelOf μ Y G T_rv A hT_pos hp_pos hp_sum) := by
let H := panelClass μ G T_rv G_meas T_meas
let wY := residWitnessY_panel μ Y G T_rv G_meas T_meas Y_memLp B_balanced
let wD := residWitnessD_panel μ D G T_rv G_meas T_meas D_meas D_binary
B_balanced
let P := panelOf μ Y G T_rv A hT_pos hp_pos hp_sum
have hMeanReg_mem : H.mem (panelMeanReg μ Y G T_rv) :=
panelMeanReg_mem_panelClass μ Y G T_rv G_meas T_meas
have hNum_tilde :
∫ ω, wD.Vtilde ω * wY.Vtilde ω ∂μ =
∫ ω, wD.Vtilde ω * Y ω ∂μ := by
have hDY_int : Integrable (fun ω => wD.Vtilde ω * Y ω) μ :=
wD.Vtilde_memLp.integrable_mul Y_memLp
have hDM_int : Integrable (fun ω => wD.Vtilde ω * panelMeanReg μ Y G T_rv ω) μ :=
wD.Vtilde_memLp.integrable_mul (H.memLp hMeanReg_mem)
calc
∫ ω, wD.Vtilde ω * wY.Vtilde ω ∂μ =
∫ ω, wD.Vtilde ω * Y ω
- wD.Vtilde ω * panelMeanReg μ Y G T_rv ω ∂μ := by
refine integral_congr_ae ?_
filter_upwards [] with ω
simp [wY, residWitnessY_panel]
ring
_ = ∫ ω, wD.Vtilde ω * Y ω ∂μ
- ∫ ω, wD.Vtilde ω * panelMeanReg μ Y G T_rv ω ∂μ :=
integral_sub hDY_int hDM_int
_ = ∫ ω, wD.Vtilde ω * Y ω ∂μ := by
rw [wD.orthogonal hMeanReg_mem]
ring
have hDen_sum :
∫ ω, wD.Vtilde ω * wD.Vtilde ω ∂μ =
∑ g, ∑ t, cellMass μ G T_rv g t
* (panelDtilde μ D G T_rv g t)^2 := by
have hF_int : Integrable (fun ω => wD.Vtilde ω * wD.Vtilde ω) μ :=
wD.Vtilde_memLp.integrable_mul wD.Vtilde_memLp
calc
∫ ω, wD.Vtilde ω * wD.Vtilde ω ∂μ =
∑ g, ∑ t, ∫ ω, (wD.Vtilde ω * wD.Vtilde ω)
* indicator {ω' | G ω' = g ∧ T_rv ω' = t}
(fun _ => (1 : ℝ)) ω ∂μ :=
integral_eq_sum_panel_cell μ (fun ω => wD.Vtilde ω * wD.Vtilde ω)
G T_rv G_meas T_meas hF_int
_ = ∑ g, ∑ t, cellMass μ G T_rv g t
* (panelDtilde μ D G T_rv g t)^2 := by
refine Finset.sum_congr rfl (fun g _ => ?_)
refine Finset.sum_congr rfl (fun t _ => ?_)
simpa [wD, residWitnessD_panel, mul_assoc] using
denom_per_cell_panel μ D G T_rv G_meas T_meas g t (hD_cell g t)
have hNum_sum :
∫ ω, wD.Vtilde ω * Y ω ∂μ =
∑ g, ∑ t, cellMass μ G T_rv g t
* panelDtilde μ D G T_rv g t
* cellMean μ Y G T_rv g t := by
have hF_int : Integrable (fun ω => wD.Vtilde ω * Y ω) μ :=
wD.Vtilde_memLp.integrable_mul Y_memLp
calc
∫ ω, wD.Vtilde ω * Y ω ∂μ =
∑ g, ∑ t, ∫ ω, (wD.Vtilde ω * Y ω)
* indicator {ω' | G ω' = g ∧ T_rv ω' = t}
(fun _ => (1 : ℝ)) ω ∂μ :=
integral_eq_sum_panel_cell μ (fun ω => wD.Vtilde ω * Y ω)
G T_rv G_meas T_meas hF_int
_ = ∑ g, ∑ t, cellMass μ G T_rv g t
* panelDtilde μ D G T_rv g t
* cellMean μ Y G T_rv g t := by
refine Finset.sum_congr rfl (fun g _ => ?_)
refine Finset.sum_congr rfl (fun t _ => ?_)
simpa [wD, residWitnessD_panel, mul_assoc] using
num_per_cell_panel μ D Y G T_rv G_meas T_meas g t (hD_cell g t)
calc
residualizedCoefficient μ (panelClass μ G T_rv G_meas T_meas)
(residWitnessY_panel μ Y G T_rv G_meas T_meas Y_memLp B_balanced)
(residWitnessD_panel μ D G T_rv G_meas T_meas D_meas D_binary
B_balanced)
= (∫ ω, wD.Vtilde ω * wY.Vtilde ω ∂μ)
/ (∫ ω, wD.Vtilde ω * wD.Vtilde ω ∂μ) := by
rfl
_ = (∫ ω, wD.Vtilde ω * Y ω ∂μ)
/ (∫ ω, wD.Vtilde ω * wD.Vtilde ω ∂μ) := by
rw [hNum_tilde]
_ = (∑ g, ∑ t, cellMass μ G T_rv g t
* panelDtilde μ D G T_rv g t
* cellMean μ Y G T_rv g t)
/ (∑ g, ∑ t, cellMass μ G T_rv g t
* (panelDtilde μ D G T_rv g t)^2) := by
rw [hNum_sum, hDen_sum]
_ = betaTWFE P := by
simp [P, panelOf, betaTWFE, VD, hLaw, hDtilde_eq, mul_assoc]