Panel.EstimandCharacterization.EventStudyContamination
Sun-Abraham: contamination of event-study coefficients under heterogeneous cohort effects and the interaction-weighted fix.
Setup 24 core · 3 supporting This file provides the finite staggered-adoption event-study system used by the Sun-Abraham characterization modules. ★ CATT_eq_zero_of_noAnticipation★ observedCellMean_eq_fixedEffects_add_CATT
Sun-Abraham Event-Study Setup
This file provides the finite staggered-adoption event-study system used by the Sun-Abraham characterization modules. It defines the cohort, period, relative-time, potential-outcome, and comparison-path primitives on which the conventional and interaction-weighted estimands are built.
A finite-cell record of a staggered-adoption event-study design over T periods, where adoption paths are finite periods or the never-treated path. It bundles a numeric encoding used to form relative event time, the finite set of supported adoption cohorts, each adoption path's population share, the cohort-period cell mass, the factual observed outcome means, the own-treatment-path mean potential outcome, and the never-treated mean potential outcomes.
Definition (Lean source)
For an event study with periods and a finite adoption cohort, the finite adoption path has that cohort's adoption date.
For an event study with periods and an adoption path, the never-treated predicate holds exactly when the path is never treated.
For an event study with periods and an adoption path, the eventually-treated predicate holds exactly when the path has a finite adoption date.
For an event-study system, an adoption cohort, and a period, relative event time is the period's calendar time minus the cohort's calendar time.
Definition (Lean source)
For an event study with periods, an adoption path, and a period, the absorbing treatment indicator equals one exactly when the path has adopted by the period, and equals zero otherwise.
For an event-study system, a finite cohort, and an integer relative time, the target-period set consists of the finite periods with that relative event time for the cohort.
Definition (Lean source)
For an event-study system and a finite cohort, the baseline-period set is the target-period set at relative event time minus one.
Definition (Lean source)
For an event-study system, a finite cohort, and an integer relative time, the admissible-cell predicate holds exactly when the cohort belongs to the event-study support and some finite period has that relative event time for the cohort.
Definition (Lean source)
For an event-study system and a finite set of relative times, the admissible-cell support consists of the supported cohort-relative-time pairs that satisfy the admissible-cell predicate.
For an event-study system, a finite set of relative times, and a relative time, the cohorts at that event time are the supported cohorts for which the relative time belongs to the set and the corresponding cell is admissible.
Definition (Lean source)
For an event-study system, a cohort, and a relative time, the cohort-relative-time cell mass is the sum of the cohort-period cell masses over the corresponding target periods.
Definition (Lean source)
For an event-study system, a cohort, and a relative time, the observed cell mean is the average of the cohort's factual observed means over the target periods, with value zero when that set is empty.
Definition (Lean source)
For an event-study system, a cohort, and a relative time, the mean cell contrast is the target-period average of the treated-path mean minus the never-treated mean, with value zero when there are no target periods.
Definition (Lean source)
For an event-study system, a cohort, and a relative time, the cohort average treatment effect on the treated is the corresponding mean cell contrast.
Definition (Lean source)
For an event-study system, an adoption path, a treated cohort, and a relative time, the path target mean is the average factual path mean over the target periods, with value zero when that set is empty.
Definition (Lean source)
For an event-study system, an adoption path, and a treated cohort, the path baseline mean is the average factual path mean over the cohort's baseline periods, with value zero when that set is empty.
Definition (Lean source)
For an event-study system, the consistency condition states that every supported cohort's factual observed mean equals its own-treatment-path mean in every period.
Definition (Lean source)
For an event-study system, the path-consistency condition states that the factual path mean equals the never-treated path mean whenever the path is untreated.
Definition (Lean source)
For an event-study system, the no-anticipation condition states that every supported cohort's own-path and never-treated means agree before adoption.
Definition (Lean source)
For an event-study system, the mean-parallel-untreated condition states that there exist cohort and period components whose sum gives an additive cohort-period function, equal to every supported cohort's never-treated mean in every period.
Definition (Lean source)
Sun-Abraham event-study causal restrictions. Field names mirror the NL artifact's assumption names.
Definition (Lean source)
No anticipation implies zero pre-treatment CATT. If the mean treated and never-treated potential outcomes for every adopting cohort coincide in every period strictly preceding that cohort's own adoption period (no anticipation), then for a cohort g in the finite adoption-cohort support and a relative event time e strictly before adoption (), the cohort-average treatment effect on the treated at cell (g, e) is zero.
Formal statement
Proof (Lean source)
Cell-mean decomposition into additive untreated fixed effects and CATT. If the factual observed outcome mean on a cohort's own periods equals its mean treated potential outcome (consistency) and the mean never-treated potential outcome admits an additive cohort/period fixed-effects representation (mean-parallel untreated paths), then for any cohort g in the finite adoption-cohort support, the average observed outcome mean over the target periods of cell (g, e) decomposes as the average, over those periods, of the additive fixed effects alpha g + lambda t plus the cohort-average treatment effect on the treated CATT g e.
Formal statement
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
pathConsistency_observed_eq_untreatedtheorem — Path-consistency, applied to an untreated comparison period, yields the observed-equals-untreated path-mean bridge used by the IW comparison-group argument.hypothesesT :sharedℕP :hPathConsistency :P.PathConsistencyt :Fin ThUntreated :absorbingTreatment h t = 0conclusionP.observedPathMean h t = P.untreatedPathMean h tProof (Lean source)
theorem pathConsistency_observed_eq_untreated (P : EventStudySystem T) (hPathConsistency : P.PathConsistency) {h : WithTop (Fin T)} {t : Fin T} (hUntreated : absorbingTreatment h t = 0) : P.observedPathMean h t = P.untreatedPathMean h t := hPathConsistency h t hUntreated -
targetPeriods_subsingleton_of_injectivetheorem — Under an injective calendar-time encoding, at most one finite period can realize a given relative time, so the target-period set of any cell is a subsingleton.hypothesesProof (Lean source)
theorem targetPeriods_subsingleton_of_injective (P : EventStudySystem T) (hInj : Injective P.time) (g : Fin T) (e : ℤ) : (P.targetPeriods g e : Set (Fin T)).Subsingleton := by intro a ha b hb simp only [Finset.mem_coe, targetPeriods, mem_filter, Finset.mem_univ, true_and] at ha hb simp only [relTime] at ha hb have hab : P.time a = P.time b := by have := ha.trans hb.symm linarith [this] exact hInj hab -
CATT_eq_sourceCATT_of_injectivetheorem — G1 faithfulness corollary. When the calendar-time map time is injective (the usual one-period-per-relative-time encoding), the cell-averaged CATT g e collapses to the source's *point* CATT_{g,e} at the unique period t realizing relative time e, i.e. treatedMean g t - untreatedMean g t.hypothesesconclusionP.CATT g e = P.treatedMean g t - P.untreatedMean g tProof (Lean source)
theorem CATT_eq_sourceCATT_of_injective (P : EventStudySystem T) (hInj : Injective P.time) {g : Fin T} {e : ℤ} {t : Fin T} (ht : t ∈ P.targetPeriods g e) : P.CATT g e = P.treatedMean g t - P.untreatedMean g t := by have hsub := P.targetPeriods_subsingleton_of_injective hInj g e have hsingleton : P.targetPeriods g e = {t} := by apply Finset.eq_singleton_iff_unique_mem.mpr refine ⟨ht, ?_⟩ intro x hx exact hsub (by simpa using hx) (by simpa using ht) unfold CATT meanCellContrast rw [hsingleton] simp
Conventional 13 core · 2 supporting This file formalizes finite-cell algebra for an event-study coefficient defined by a projection on the listed finite cohorts and declared relative-time cells. ★ contamination_representation★ contamination_representation_split★ apparent_pretrends_from_post_treatment
Listed-Cohort Cell-Grid Event Study
This file formalizes finite-cell algebra for an event-study coefficient defined by a projection on the listed finite cohorts and declared relative-time cells. It expresses that coefficient as a generally signed weighted sum of cohort-relative-time treatment effects under supplied residualization and support conditions. The projection does not include the never-treated path and is not asserted to equal a full-population two-way fixed-effects regression.
For two relative times, the event-time indicator equals one when they are equal and zero otherwise.
Definition (Lean source)
An event-study cell-grid design on a finite system records the relative-time support used in its cell expansion, the included event-time regressors, an omitted-event metadata label, the displayed event time, the displayed indicator's cellwise residual, and the displayed cell-grid coefficient.
Definition (Lean source)
For a finite time horizon, an event-study system, a cell-grid design, and a cohort-period function, the event-study nuisance condition holds exactly when the function is the sum of a cohort-and-period additive component and a linear combination of the included relative-time indicators other than the displayed indicator, for every cohort in the system and every period.
Definition (Lean source)
For a finite time horizon, an event-study system, a cohort-period function, a cohort, and a relative time, the cell average is the average of that function over the periods in which the cohort has the given relative time.
Definition (Lean source)
Finite-cell residualization record for the cell-grid coefficient.
Definition (Lean source)
For a finite time horizon, an event-study system, and a cell-grid design, the residualized denominator is the sum over admissible cells of cell mass times the design residual times the indicator for the displayed event time.
Definition (Lean source)
For a finite time horizon, an event-study system, and a cell-grid design, the residualized numerator is the sum over admissible cells of cell mass times the design residual times the observed cell mean.
Definition (Lean source)
For a finite time horizon, an event-study system, and an event-study design, the cell-grid coefficient ratio is the residualized numerator divided by the residualized denominator.
Definition (Lean source)
Transparent finite support bookkeeping for the conventional cell expansion. It records that the explicit event-time support is the finite universe over which the displayed theorem is expanded, without asserting the headline contamination formula itself.
Definition (Lean source)
For a finite time horizon, an event-study system, a cell-grid design, a cohort, and a relative time, the cell-grid contamination weight is that cell's mass times its design residual, divided by the residualized denominator.
Definition (Lean source)
Finite-cell contamination representation. For an event-study system and cell-grid design, if observed outcomes equal the own-path potential-outcome means, never-treated means obey additive parallel trends, Rdot is orthogonal to every event-study nuisance function, the residualized denominator is strictly positive, D.mu equals its FWL residualized ratio, and the included, displayed, and admissible event times have finite support, then D.mu equals the contamination-weighted sum of CATTs over admissible cells.
Formal statement
Proof (Lean source)
For an event-study system and cell-grid design, if observed outcomes equal the own-path potential-outcome means, never-treated means obey additive parallel trends, the design satisfies the finite-cell orthogonality conditions, the residualized denominator is strictly positive, D.mu equals its FWL residualized ratio, and the included, displayed, and admissible event times have finite support, then D.mu splits into its displayed-event term and all other admissible-cell terms.
Formal statement
Proof (Lean source)
For an event-study system and cell-grid design, if the displayed event is a lead, the consistency, parallel-trends, and no-anticipation restrictions hold, Rdot is orthogonal to every event-study nuisance function, the residualized denominator is strictly positive, D.mu equals its FWL residualized ratio, and the included, displayed, and admissible event times have finite support, then D.mu is a generally signed contamination-weighted sum of nonnegative-event-time CATTs.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
desired_event_weights_sum_onetheorem — Desired-event-time weights sum to one.hypothesesT :sharedℕP :D :P.ConventionalDesignhDisplayedExpansion :∑ ge ∈ P.admissibleCells D.eventSupport, P.cellMassAtEvent ge.1 ge.2 * D.Rdot ge.1 ge.2 * eventIndicator D.displayedEvent ge.2= ∑ g ∈ P.cohortsAtEvent D.eventSupport D.displayedEvent, P.cellMassAtEvent g D.displayedEvent * D.Rdot g D.displayedEventhDenomPos :0 < P.residualDenom Dconclusion∑ g ∈ P.cohortsAtEvent D.eventSupport D.displayedEvent, P.omega D g D.displayedEvent = 1Proof (Lean source)
theorem desired_event_weights_sum_one (P : EventStudySystem T) (D : P.ConventionalDesign) (hDisplayedExpansion : ∑ ge ∈ P.admissibleCells D.eventSupport, P.cellMassAtEvent ge.1 ge.2 * D.Rdot ge.1 ge.2 * eventIndicator D.displayedEvent ge.2 = ∑ g ∈ P.cohortsAtEvent D.eventSupport D.displayedEvent, P.cellMassAtEvent g D.displayedEvent * D.Rdot g D.displayedEvent) (hDenomPos : 0 < P.residualDenom D) : ∑ g ∈ P.cohortsAtEvent D.eventSupport D.displayedEvent, P.omega D g D.displayedEvent = 1 := by have hDenom_ne : P.residualDenom D ≠ 0 := ne_of_gt hDenomPos calc ∑ g ∈ P.cohortsAtEvent D.eventSupport D.displayedEvent, P.omega D g D.displayedEvent = (∑ g ∈ P.cohortsAtEvent D.eventSupport D.displayedEvent, P.cellMassAtEvent g D.displayedEvent * D.Rdot g D.displayedEvent) / P.residualDenom D := by simp [omega, Finset.sum_div] _ = P.residualDenom D / P.residualDenom D := by rw [← hDisplayedExpansion] rfl _ = 1 := div_self hDenom_ne -
other_included_event_weights_sum_zerotheorem — Other included-event-time weights sum to zero.hypothesesT :sharedℕP :D :P.ConventionalDesigne :ℤhOtherZero :∑ g ∈ P.cohortsAtEvent D.eventSupport e, P.cellMassAtEvent g e * D.Rdot g e = 0hDenomPos :0 < P.residualDenom Dconclusion∑ g ∈ P.cohortsAtEvent D.eventSupport e, P.omega D g e = 0Proof (Lean source)
theorem other_included_event_weights_sum_zero (P : EventStudySystem T) (D : P.ConventionalDesign) {e : ℤ} (hOtherZero : ∑ g ∈ P.cohortsAtEvent D.eventSupport e, P.cellMassAtEvent g e * D.Rdot g e = 0) (hDenomPos : 0 < P.residualDenom D) : ∑ g ∈ P.cohortsAtEvent D.eventSupport e, P.omega D g e = 0 := by have _ : P.residualDenom D ≠ 0 := ne_of_gt hDenomPos calc ∑ g ∈ P.cohortsAtEvent D.eventSupport e, P.omega D g e = (∑ g ∈ P.cohortsAtEvent D.eventSupport e, P.cellMassAtEvent g e * D.Rdot g e) / P.residualDenom D := by simp [omega, Finset.sum_div] _ = 0 / P.residualDenom D := by rw [hOtherZero] _ = 0 := zero_div _
CellGrid 10 core · 6 supporting This file derives finite-cell residualization and ratio identities from a weighted projection on the listed-cohort-by-relative-time cell grid. ★ cellGrid_mu_eq_conventionalMuRatio★ cellGrid_provides_residualization
Listed-Cohort Cell-Grid Projection
This file derives finite-cell residualization and ratio identities from a weighted projection on the listed-cohort-by-relative-time cell grid. The grid omits the never-treated path and every cell outside the declared event support, so it is not identified here with a full-population TWFE regression. The resulting bridge supplies the orthogonality and normal-equation inputs used by the contamination representation.
For a finite time horizon, an event-study system, and a cell-grid design, the cell index is the collection of admissible cohort--relative-time cells in that design.
Definition (Lean source)
For a finite time horizon, an event-study system, and a cell-grid design, the total admissible cell mass is the sum of the population masses of all admissible cohort--relative-time cells.
Definition (Lean source)
For a finite time horizon, an event-study system, and a cell-grid design, if every admissible cohort--relative-time cell has strictly positive population mass and at least one admissible cell exists, the cell-grid weighted support is the finite population of admissible cells, weighted by each cell's mass divided by total admissible cell mass.
Definition (Lean source)
For a finite time horizon, an event-study system, and a cell-grid design, the generators of the cell-nuisance space are precisely the functions on admissible cells obtained by averaging an event-study nuisance function within each cohort--relative-time cell.
Definition (Lean source)
For a finite time horizon, an event-study system, and a cell-grid design, the cell-nuisance space is the linear span of all cell-level averages of event-study nuisance functions.
Definition (Lean source)
For a finite time horizon, an event-study system, and a cell-grid design, the cell-grid regressor assigns one to an admissible cell exactly when its relative time is the displayed event time, and zero otherwise.
Definition (Lean source)
For a finite time horizon, an event-study system, and a cell-grid design, the cell-grid outcome assigns to each admissible cohort--relative-time cell its observed mean outcome.
Definition (Lean source)
Cell-grid residualization input. An event-study design on a finite system is backed by a well-posed weighted cell-grid projection when every admissible cell has positive mass, the grid is nonempty, the residualized regressor has positive energy, the recorded residual is the projected displayed indicator, and a nuisance fit satisfies both normal equations.
Definition (Lean source)
Cell-grid FWL bridge. Under cell-grid residualization of the event-study design, the recorded coefficient equals the FWL residualized ratio on the cell grid.
Formal statement
Proof (Lean source)
For an event-study design D over an event-study system P, if every admissible cell has strictly positive population mass, the collection of admissible cells is nonempty, and Rdot agrees cellwise with the weighted cell-grid projection residual, then the three finite-cell orthogonality conditions hold for D as projection consequences.
Formal statement
Proof (Lean source)
6 supporting declarations (lemmas, instances)
-
ip_cellSupportlemma — ip → cell-sum. The cell-grid weighted inner product of two cell functions reproduces the finite-cell sum (divided by the total mass Z). This is the bridge that turns weighted-projection facts into the finite-cell orthogonality conditions.hypothesesProof (Lean source)
lemma ip_cellSupport (P : EventStudySystem T) (D : P.ConventionalDesign) (hpos : ∀ ge ∈ P.admissibleCells D.eventSupport, 0 < P.cellMassAtEvent ge.1 ge.2) (hne : (P.admissibleCells D.eventSupport).Nonempty) (A B : Fin T × ℤ → ℝ) : (P.cellSupport D hpos hne).ip (fun cell => A cell.val) (fun cell => B cell.val) = (∑ ge ∈ P.admissibleCells D.eventSupport, P.cellMassAtEvent ge.1 ge.2 * A ge * B ge) / P.cellTotalMass D := by classical rw [WeightedSupport.ip_def] have hobs : (P.cellSupport D hpos hne).observed = (Finset.univ : Finset (P.CellIndex D)) := rfl rw [hobs] rw [show (∑ cell : P.CellIndex D, (P.cellSupport D hpos hne).weight cell * A cell.val * B cell.val) = ∑ cell : P.CellIndex D, (fun ge : Fin T × ℤ => P.cellMassAtEvent ge.1 ge.2 / P.cellTotalMass D * A ge * B ge) cell.val from rfl] rw [Finset.sum_coe_sort (P.admissibleCells D.eventSupport) (fun ge => P.cellMassAtEvent ge.1 ge.2 / P.cellTotalMass D * A ge * B ge)] rw [Finset.sum_div] refine Finset.sum_congr rfl (fun ge _ => ?_) ring -
cellAverage_mem_cellNuisancelemma — Every cell-evaluated nuisance function lies in the cell-nuisance subspace.hypothesesT :sharedℕP :D :P.ConventionalDesignhN :P.IsEventStudyNuisance D hCellconclusion(fun cell : P.CellIndex D => P.cellAverage hCell cell.val.1 cell.val.2) ∈ P.cellNuisance DProof (Lean source)
lemma cellAverage_mem_cellNuisance (P : EventStudySystem T) (D : P.ConventionalDesign) {hCell : Fin T → Fin T → ℝ} (hN : P.IsEventStudyNuisance D hCell) : (fun cell : P.CellIndex D => P.cellAverage hCell cell.val.1 cell.val.2) ∈ P.cellNuisance D := Submodule.subset_span ⟨hCell, hN, rfl⟩ -
cellAverage_eventIndicatorlemma — The cell average of the relative-time indicator 1{relTime = e}, evaluated on a nonempty cell (g, e'), is the cell-level indicator 1{e' = e}.hypothesesconclusionP.cellAverage (fun g t => eventIndicator e (P.relTime g t)) g e' = eventIndicator e e'Proof (Lean source)
lemma cellAverage_eventIndicator (P : EventStudySystem T) {e : ℤ} {g : Fin T} {e' : ℤ} (hne : (P.targetPeriods g e').Nonempty) : P.cellAverage (fun g t => eventIndicator e (P.relTime g t)) g e' = eventIndicator e e' := by classical have hcard : ((P.targetPeriods g e').card : ℝ) ≠ 0 := by have : 0 < (P.targetPeriods g e').card := Finset.card_pos.mpr hne exact_mod_cast this.ne' unfold EventStudySystem.cellAverage have hconst : ∀ t ∈ P.targetPeriods g e', eventIndicator e (P.relTime g t) = eventIndicator e e' := by intro t ht have hrel : P.relTime g t = e' := by simpa [EventStudySystem.targetPeriods] using ht rw [hrel] rw [Finset.sum_congr rfl hconst, Finset.sum_const, nsmul_eq_mul, ← mul_assoc, inv_mul_cancel₀ hcard, one_mul] -
eventIndicator_mem_cellNuisancelemma — A non-displayed included relative-time indicator lies in the cell-nuisance subspace (it is the cell average of the corresponding event-study nuisance).hypothesesT :sharedℕP :D :P.ConventionalDesigne :ℤhe_inc :e ∈ D.includedEventshe_ne :e ≠ D.displayedEventconclusion(fun cell : P.CellIndex D => eventIndicator e cell.val.2) ∈ P.cellNuisance DProof (Lean source)
lemma eventIndicator_mem_cellNuisance (P : EventStudySystem T) (D : P.ConventionalDesign) {e : ℤ} (he_inc : e ∈ D.includedEvents) (he_ne : e ≠ D.displayedEvent) : (fun cell : P.CellIndex D => eventIndicator e cell.val.2) ∈ P.cellNuisance D := by classical have hN : P.IsEventStudyNuisance D (fun g t => eventIndicator e (P.relTime g t)) := by refine ⟨fun _ _ => 0, ⟨fun _ => 0, fun _ => 0, fun g t => by simp⟩, fun k => if k = e then 1 else 0, ?_⟩ intro g _ t simp only [zero_add] rw [Finset.sum_eq_single e] · simp · intro k _ hkne; simp [hkne] · intro hnot exact absurd (Finset.mem_filter.mpr ⟨he_inc, he_ne⟩) hnot have heq : (fun cell : P.CellIndex D => P.cellAverage (fun g t => eventIndicator e (P.relTime g t)) cell.val.1 cell.val.2) = fun cell : P.CellIndex D => eventIndicator e cell.val.2 := by funext cell have hmem : cell.val ∈ (P.cohorts.product D.eventSupport).filter (fun ge => P.AdmissibleCell ge.1 ge.2) := cell.property obtain ⟨_, hnonempty⟩ := (Finset.mem_filter.mp hmem).2 exact P.cellAverage_eventIndicator (e := e) hnonempty rw [← heq] exact P.cellAverage_mem_cellNuisance D hN -
sum_admissible_mul_eventIndicatorlemma — Cell-grid filtering identity. Weighting an admissible-cell sum by the relative-time indicator 1{e = e'} collapses it to a sum over the cohorts observed at relative time e'. Pure finite algebra; no residualization needed. This is the engine behind hDisplayedExpansion and hOtherIncludedOrthogonal.hypothesesconclusion∑ ge ∈ P.admissibleCells D.eventSupport, f ge.1 ge.2 * eventIndicator e' ge.2= ∑ g ∈ P.cohortsAtEvent D.eventSupport e', f g e'Proof (Lean source)
lemma sum_admissible_mul_eventIndicator (P : EventStudySystem T) (D : P.ConventionalDesign) (e' : ℤ) (f : Fin T → ℤ → ℝ) : ∑ ge ∈ P.admissibleCells D.eventSupport, f ge.1 ge.2 * eventIndicator e' ge.2 = ∑ g ∈ P.cohortsAtEvent D.eventSupport e', f g e' := by classical have hfilter : (P.admissibleCells D.eventSupport).filter (fun ge => ge.2 = e') = (P.cohortsAtEvent D.eventSupport e').map ⟨fun g => (g, e'), fun a b h => congrArg fst h⟩ := by ext ge rcases ge with ⟨g, e⟩ simp only [admissibleCells, product_eq_sprod, mem_filter, mem_product, cohortsAtEvent, mem_map] constructor · rintro ⟨⟨⟨hg, heSupport⟩, hAdm⟩, rfl⟩ exact ⟨g, ⟨hg, heSupport, hAdm⟩, rfl⟩ · rintro ⟨a, ⟨ha, hSupport, hAdm⟩, hEq⟩ have hEq' : (a, e') = (g, e) := hEq injection hEq' with h1 h2 subst h1 subst h2 exact ⟨⟨⟨ha, hSupport⟩, hAdm⟩, rfl⟩ calc ∑ ge ∈ P.admissibleCells D.eventSupport, f ge.1 ge.2 * eventIndicator e' ge.2 = ∑ ge ∈ P.admissibleCells D.eventSupport, if ge.2 = e' then f ge.1 e' else 0 := by refine Finset.sum_congr rfl (fun ge _ => ?_) unfold EventStudySystem.eventIndicator by_cases h : ge.2 = e' · rw [h]; simp · simp [h] _ = ∑ ge ∈ (P.admissibleCells D.eventSupport).filter (fun ge => ge.2 = e'), f ge.1 e' := by rw [Finset.sum_filter] _ = ∑ g ∈ P.cohortsAtEvent D.eventSupport e', f g e' := by rw [hfilter, Finset.sum_map] rfl -
tildeX_eq_Rdotlemma — Under cell-grid residualization, the residualized displayed-event regressor equals the design residual at every admissible cohort--relative-time cell.hypothesesconclusion(P.cellSupport D h.hCellMassPos h.hCellNonempty).tildeX (P.cellNuisance D) (P.cellRegressor D)= fun cell => D.Rdot cell.val.1 cell.val.2Proof (Lean source)
lemma tildeX_eq_Rdot (h : P.CellGridResidualization D) : (P.cellSupport D h.hCellMassPos h.hCellNonempty).tildeX (P.cellNuisance D) (P.cellRegressor D) = fun cell => D.Rdot cell.val.1 cell.val.2 := by funext cell; exact (h.hRdotResidual cell).symm
InteractionWeighted 12 core · 1 supporting This file develops the finite-cell interaction-weighted event-study estimand for the Sun-Abraham framework. ★ IW_Delta_eq_CATT★ IW_convex_characterization
Sun-Abraham Interaction-Weighted Event Study
This file develops the finite-cell interaction-weighted event-study estimand for
the Sun-Abraham framework. It records the comparison-group contrasts and
aggregation weights that make the interaction-weighted coefficient a convex
average of target cohort-specific effects, proving IW_Delta_eq_CATT and
IW_convex_characterization.
Interaction-weighted finite DID design for a fixed event time.
Definition (Lean source)
For a finite time horizon, an event-study system, an interaction-weighted design, and a cohort, the observed target mean is the average observed outcome of that cohort over the periods at the design's specified relative time.
Definition (Lean source)
For a finite time horizon, an event-study system, and a cohort, the observed baseline mean is the average observed outcome of that cohort over its baseline periods, defined at relative time .
Definition (Lean source)
For a finite time horizon, an event-study system, an interaction-weighted design, and a cohort, the comparison mass is the total population share of the cohorts in that cohort's comparison group.
Definition (Lean source)
For a finite time horizon, an event-study system, an interaction-weighted design, and a cohort, the comparison mean change is the comparison-group population-share-weighted average of each comparison path's change from the cohort's baseline periods to its target periods.
Definition (Lean source)
For a finite time horizon, an event-study system, an interaction-weighted design, and a cohort, the difference-in- differences contrast is the treated cohort's observed target-minus- baseline mean change minus the corresponding comparison-group mean change.
Definition (Lean source)
For a finite time horizon, an event-study system, an interaction-weighted design, and a cohort, the interaction- weighted cohort contrast is that cohort's difference-in-differences contrast.
Definition (Lean source)
For a finite time horizon, an event-study system, and an interaction-weighted design, the interaction-weighted event-study estimand is the sum, over all eligible cohorts, of each aggregation weight times that cohort's interaction-weighted contrast.
Definition (Lean source)
IW support restrictions for eligible cohorts and their comparison groups.
Definition (Lean source)
Comparison-group parallel trends for the IW DID contrast.
Definition (Lean source)
For an event-study system P and interaction-weighted design I, if consistency, no-anticipation, and path-consistency hold, every eligible cohort's comparison-group mean change from baseline to target period matches its own untreated-mean change, every eligible cohort is a genuine cohort of the system, and every comparison unit is untreated throughout the baseline and target periods, then for any eligible cohort g, its interaction-weighted DID contrast Delta I g equals the cohort-relative-time average treatment effect CATT g I.eventTime.
Formal statement
Proof (Lean source)
For an event-study system P and interaction-weighted design I, if consistency, no-anticipation, and path-consistency hold, every eligible cohort's comparison-group mean change from baseline to target period matches its own untreated-mean change, the eligibility, baseline, target, and comparison-group support conditions of IWSupport hold, the aggregation weights rho are nonnegative and sum to one over the eligible cohorts, and every eligible cohort's CATT at the fixed event time lies between bounds lo and hi, then each cohort's DID contrast equals its CATT, the interaction-weighted estimand nuIW I equals the rho-weighted average of those CATTs, and nuIW I itself lies between lo and hi — a genuine convex average with no contamination from other relative times.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
sum_convex_mem_Icctheorem — Finite convex-combination bound. If the weights w are nonnegative and sum to one, then any nonnegative-weighted average of values lying in [lo, hi] again lies in [lo, hi]. This is the algebraic content of "convex combination" used to certify that the IW estimand is a genuine convex average of the target CATTs (no contamination).hypothesesι :Type*s :Finset ιw f :ι → ℝlo hi :ℝhw :∀ i ∈ s, 0 ≤ w ihsum :∑ i ∈ s, w i = 1hlo :∀ i ∈ s, lo ≤ f ihhi :∀ i ∈ s, f i ≤ hiconclusionconclusion 1lo ≤ ∑ i ∈ s, w i * f iconclusion 2∑ i ∈ s, w i * f i ≤ hiProof (Lean source)
theorem sum_convex_mem_Icc {ι : Type*} (s : Finset ι) (w f : ι → ℝ) {lo hi : ℝ} (hw : ∀ i ∈ s, 0 ≤ w i) (hsum : ∑ i ∈ s, w i = 1) (hlo : ∀ i ∈ s, lo ≤ f i) (hhi : ∀ i ∈ s, f i ≤ hi) : lo ≤ ∑ i ∈ s, w i * f i ∧ ∑ i ∈ s, w i * f i ≤ hi := by constructor · calc lo = ∑ i ∈ s, w i * lo := by rw [← Finset.sum_mul, hsum, one_mul] _ ≤ ∑ i ∈ s, w i * f i := by apply Finset.sum_le_sum intro i hi' exact mul_le_mul_of_nonneg_left (hlo i hi') (hw i hi') · calc ∑ i ∈ s, w i * f i ≤ ∑ i ∈ s, w i * hi := by apply Finset.sum_le_sum intro i hi' exact mul_le_mul_of_nonneg_left (hhi i hi') (hw i hi') _ = hi := by rw [← Finset.sum_mul, hsum, one_mul]
Contamination 3 core · 0 supporting This file provides public contamination theorems for an event-study coefficient defined by a weighted projection on the listed finite cohorts and declared event-support cells. ★ contamination_representation_of_cellGrid★ contamination_representation_split_of_cellGrid★ apparent_pretrends_from_post_treatment_of_cellGrid
Listed-Cohort Cell-Grid Contamination Representation
This file provides public contamination theorems for an event-study coefficient defined by a weighted projection on the listed finite cohorts and declared event-support cells. It derives the needed residualization identities and applies the finite-cell algebra to obtain the displayed contamination formulas. These results do not identify that restricted projection with a full-population TWFE regression.
Cell-grid contamination representation. For the coefficient D.mu of a cell-grid design, if observed outcomes equal the own-path potential-outcome means, never-treated means obey additive parallel trends, the relevant event times have finite support, and the weighted cell-grid projection input is supplied, then D.mu equals the contamination-weighted sum of CATTs over admissible cells.
Formal statement
Proof (Lean source)
Cell-grid contamination split. For the coefficient D.mu of a cell-grid design, if the consistency, parallel-trends, and no-anticipation restrictions hold, the relevant event times have finite support, and the weighted cell-grid projection input is supplied, then D.mu splits into its displayed-event term and all other admissible-cell terms.
Formal statement
Proof (Lean source)
Cell-grid apparent pretrends. For the coefficient D.mu of a cell-grid design, if the displayed event is a lead, the consistency, parallel-trends, and no-anticipation restrictions hold, the relevant event times have finite support, and the weighted cell-grid projection input is supplied, then D.mu is a generally signed contamination-weighted sum of nonnegative-event-time CATTs.
Formal statement
Proof (Lean source)
PopulationBridge 10 core · 8 supporting This file constructs a finite EventStudySystem from a probability space with adoption-path potential outcomes, defining its mean fields as totalized cohort-cell means and deriving the event-study causal restrictions from ★ toSystem_CATT_eq_po_contrast★ contamination_representation_population★ IW_convex_characterization_population
Event-study population bridge
This file constructs a finite EventStudySystem from a probability space with
adoption-path potential outcomes, defining its mean fields as totalized
cohort-cell means and deriving the event-study causal restrictions from the
underlying potential-outcome structure.
A staggered-adoption event-study population: a probability space carrying a realized adoption cohort G — with every cohort cell measurable — a calendar-time map time that is strictly increasing in the period index, a finite set cohorts of adoption cohorts in the event-study support, and adoption-path–indexed potential outcomes Ypath t h ω = Y_{ωt}(h) satisfying structural no-anticipation: in any period where a path is untreated, its outcome equals the never-treated outcome, for every unit.
Definition (Lean source)
For an event-study population and an adoption path , the adoption-path cell is the event consisting exactly of units whose realized adoption path is .
Definition (Lean source)
For an event-study population and an adoption path , the adoption-path cell mass is the real-valued probability mass of the units whose realized adoption path is .
Definition (Lean source)
For an event-study population, a real-valued unit-level function, and an adoption path, the adoption-path cell mean is the normalized restricted integral of the function over the event that the realized adoption path equals the given path, with value zero when that event has zero probability.
Definition (Lean source)
For an event-study population , a finite period , and a unit , the observed outcome is that unit's potential outcome at under its realized adoption path.
Definition (Lean source)
For an event-study population , the induced event-study system has the population's calendar-time map and supported cohorts, and defines every cohort share, cell mass, and outcome-mean field as the corresponding adoption-path cell probability or totalized cell mean.
Definition (Lean source)
For an event-study population , the outcome-integrability condition states that the potential outcome under every finite period and every adoption path is integrable with respect to the population measure.
Definition (Lean source)
Potential-outcome anchoring certificate. For a population satisfying the event-study setup, the induced cohort contrast at a cohort and relative time equals the relevant-period average of a difference of totalized means, so the estimand is tied to population potential-outcome data rather than free-standing reals.
Formal statement
Proof (Lean source)
Population-anchored cell-grid contamination representation (headline). The projection coefficient on listed finite cohorts and declared event-support cells is the generally signed contamination-weighted sum of the induced totalized cohort contrasts when the never-treated potential outcome obeys additive parallel trends, the relevant event times have finite support, and the coefficient comes from the stated weighted cell-grid projection. Consistency and no-anticipation follow from the potential-outcome structure rather than being imposed separately.
Formal statement
Proof (Lean source)
Population interaction-weighted characterization (headline). The interaction-weighted estimand for a staggered-adoption population and design is a bounded convex average without cross-event-time contamination under comparison-group parallel trends, valid cohort, period, and comparison-group support, nonnegative aggregation weights, weights summing to one, and the stated cohortwise bounds.
Formal statement
Proof (Lean source)
8 supporting declarations (lemmas, instances)
-
cellMean_congr_ontheorem — Event-level means agree when the integrands agree pointwise on the adoption-path cell.hypothesesT :sharedℕE :f g :E.Ω → ℝheq :∀ ω ∈ E.cell h, f ω = g ωconclusionE.cellMean f h = E.cellMean g hProof (Lean source)
theorem cellMean_congr_on (E : EventStudyPopulation T) {f g : E.Ω → ℝ} (h : WithTop (Fin T)) (heq : ∀ ω ∈ E.cell h, f ω = g ω) : E.cellMean f h = E.cellMean g h := eventCondExp_congr_on E.μ (E.Gcell_meas h) heq -
cellMean_subtheorem — Event-level means are additive over subtraction of integrable integrands.hypothesesT :sharedℕE :f g :E.Ω → ℝhf :IntegrableOn f (E.cell h) E.μhg :IntegrableOn g (E.cell h) E.μconclusionE.cellMean (f - g) h = E.cellMean f h - E.cellMean g hProof (Lean source)
theorem cellMean_sub (E : EventStudyPopulation T) {f g : E.Ω → ℝ} (h : WithTop (Fin T)) (hf : IntegrableOn f (E.cell h) E.μ) (hg : IntegrableOn g (E.cell h) E.μ) : E.cellMean (f - g) h = E.cellMean f h - E.cellMean g h := eventCondExp_sub E.μ (E.cell h) hf hg -
observed_eqOn_celltheorem — On the cohort cell {G = finitePath g}, the observed outcome equals the own-path potential outcome — the pointwise content of consistency.hypothesesconclusionE.observed t ω = E.Ypath t (EventStudySystem.finitePath g) ωProof (Lean source)
theorem observed_eqOn_cell (E : EventStudyPopulation T) (g : Fin T) (t : Fin T) : ∀ ω ∈ E.cell (EventStudySystem.finitePath g), E.observed t ω = E.Ypath t (EventStudySystem.finitePath g) ω := by intro ω hω have hG : E.G ω = EventStudySystem.finitePath g := by simpa [cell] using hω simp [observed, hG] -
toSystem_consistencytheorem — Consistency is derived. The observed cohort mean equals the own-path potential-outcome mean, because the observed outcome is the potential outcome under the realized path.Proof (Lean source)
theorem toSystem_consistency (E : EventStudyPopulation T) : (E.toSystem).Consistency := by intro g _hg t simpa [toSystem] using E.cellMean_congr_on (EventStudySystem.finitePath g) (E.observed_eqOn_cell g t) -
toSystem_noAnticipationtheorem — No-anticipation is derived from structural no-anticipation: on a pre-adoption period the own-path and never-treated potential-outcome means coincide, so their cohort means do.Proof (Lean source)
theorem toSystem_noAnticipation (E : EventStudyPopulation T) : (E.toSystem).NoAnticipation := by intro g _hg t hlt have htg : t < g := E.time_strictMono.lt_iff_lt.mp hlt have habs : EventStudySystem.absorbingTreatment (T := T) (EventStudySystem.finitePath g) t = 0 := by have hnotle : ¬ (EventStudySystem.finitePath g) ≤ (t : WithTop (Fin T)) := by simp only [EventStudySystem.finitePath, AdoptionPath.finite, not_le] exact_mod_cast htg simp [EventStudySystem.absorbingTreatment, AdoptionPath.absorbingTreatment_eq, hnotle] simpa [toSystem] using E.cellMean_congr_on (EventStudySystem.finitePath g) (fun ω _ => E.hNoAnt (EventStudySystem.finitePath g) t ω habs) -
toSystem_pathConsistencytheorem — Path-consistency is derived: on a period where comparison path h is untreated, the observed path mean equals the never-treated path mean.Proof (Lean source)
theorem toSystem_pathConsistency (E : EventStudyPopulation T) : (E.toSystem).PathConsistency := by intro h t huntreated simpa [toSystem] using E.cellMean_congr_on h (fun ω hω => by have hG : E.G ω = h := by simpa [cell] using hω have h1 : E.observed t ω = E.Ypath t h ω := by simp [observed, hG] rw [h1] exact E.hNoAnt h t ω huntreated) -
toSystem_causalRestrictionstheorem — Bundle: the induced system satisfies the Sun-Abraham causal restrictions, given the additive parallel-trends hypothesis. Consistency and no-anticipation are derived; only parallel trends is assumed.hypothesesconclusion(E.toSystem).EventStudyCausalRestrictions where hConsistencyProof (Lean source)
theorem toSystem_causalRestrictions (E : EventStudyPopulation T) (hPar : (E.toSystem).MeanParallelUntreated) : (E.toSystem).EventStudyCausalRestrictions where hConsistency := E.toSystem_consistency hNoAnticipation := E.toSystem_noAnticipation hMeanParallelUntreated := hPar -
toSystem_CATT_eq_meanDifftheorem — Integrability combines the two totalized cell means. For an event-study population, integrability of every potential-outcome slice, and a cohort and relative time, CATT is the target-period average of a totalized cell mean difference.hypothesesconclusion(E.toSystem).CATT g e= (((E.toSystem).targetPeriods g e).card : ℝ)⁻¹ * ∑ t ∈ (E.toSystem).targetPeriods g e, E.cellMean (E.Ypath t (EventStudySystem.finitePath g) - E.Ypath t ⊤) (EventStudySystem.finitePath g)Proof (Lean source)
theorem toSystem_CATT_eq_meanDiff (E : EventStudyPopulation T) (hInt : E.OutcomesIntegrable) (g : Fin T) (e : ℤ) : (E.toSystem).CATT g e = (((E.toSystem).targetPeriods g e).card : ℝ)⁻¹ * ∑ t ∈ (E.toSystem).targetPeriods g e, E.cellMean (E.Ypath t (EventStudySystem.finitePath g) - E.Ypath t ⊤) (EventStudySystem.finitePath g) := by rw [toSystem_CATT_eq_po_contrast] congr 1 refine Finset.sum_congr rfl (fun t _ => ?_) rw [E.cellMean_sub (EventStudySystem.finitePath g) (hInt t (EventStudySystem.finitePath g)).integrableOn (hInt t ⊤).integrableOn]