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 of each period used to form relative event time, the finite set of adoption cohorts in the event-study support, each adoption path's population share, and the cohort-period cell mass, together with, by cohort or by comparison adoption path, the factual observed outcome mean, the mean potential outcome under the cohort's own treatment path, and the mean never-treated potential outcome.
Definition (Lean source)
For an event study with periods and a finite adoption cohort , the finite adoption path is the path with adoption date .
For an event study with periods and an adoption path , the never-treated predicate holds exactly when is the never-treated path.
For an event study with periods and an adoption path , the eventually-treated predicate holds exactly when has a finite adoption date.
For an event-study system , an adoption cohort , and a period , relative event time is the integer calendar time of minus the integer calendar time of .
Definition (Lean source)
For an event study with periods, an adoption path , and a period , the absorbing treatment indicator equals one exactly when has adopted by , and equals zero otherwise.
For an event-study system , a finite cohort , and an integer relative time , the target-period set consists of exactly the finite periods whose relative event time for cohort is .
Definition (Lean source)
For an event-study system and a finite cohort , the baseline-period set consists of exactly the target periods 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 system's event-study support and at least one finite period has relative event time for that cohort.
Definition (Lean source)
For an event-study system and a finite set of relative times, the admissible-cell support is the finite set of cohort-relative-time pairs that use a supported cohort and a relative time in and satisfy the admissible-cell predicate.
For an event-study system , a finite set of relative times, and a relative time , the cohorts at event time are exactly the supported cohorts for which belongs to and the cohort-relative-time 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 all target periods for .
Definition (Lean source)
For an event-study system , a cohort , and a relative time , the observed cell mean is the arithmetic average of that cohort's factual observed outcome means over all target periods for ; it is zero when there are no such periods.
Definition (Lean source)
For an event-study system , a cohort , and a relative time , the mean cell contrast is the arithmetic average, over all target periods for , of the treated-path mean potential outcome minus the never-treated mean potential outcome; it is zero when there are no such 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 mean cell contrast for .
Definition (Lean source)
For an event-study system , an adoption path , a treated cohort , and a relative time , the path target mean is the arithmetic average of 's factual observed outcome mean over the target periods for ; it is 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 arithmetic average of 's factual observed outcome mean over cohort 's baseline periods; it is zero when that set is empty.
Definition (Lean source)
For an event-study system , the consistency condition states that every cohort in the event-study support has its factual observed outcome mean equal to its own-treatment-path mean potential outcome in every finite period.
Definition (Lean source)
For an event-study system , the path-consistency condition states that, for every adoption path and every finite period in which that path is untreated, the factual observed path mean equals the never-treated potential-outcome path mean.
Definition (Lean source)
For an event-study system , the no-anticipation condition states that, for every supported cohort and every finite period strictly before that cohort's adoption date in calendar time, the own-treatment-path and never-treated mean potential outcomes are equal.
Definition (Lean source)
For an event-study system , the mean-parallel-untreated condition states that there exist cohort and period components such that their sum gives an additive cohort-period function and every supported cohort's never-treated mean potential outcome equals that function in every finite 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 the finite-cell algebra for the conventional two-way fixed effects event-study coefficient in the Sun-Abraham setting. ★ contamination_representation★ contamination_representation_split★ apparent_pretrends_from_post_treatment
Sun-Abraham Conventional Event Study
This file formalizes the finite-cell algebra for the conventional two-way fixed effects event-study coefficient in the Sun-Abraham setting. It expresses the coefficient as a weighted average of cohort-relative-time treatment effects under supplied residualization, support, and integrability conditions.
For two relative times, the event-time indicator equals one when they are equal and zero otherwise.
Definition (Lean source)
Conventional event-study finite design for the coefficient on displayedEvent.
Definition (Lean source)
For a finite time horizon, an event-study system, a conventional 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 conventional coefficient.
Definition (Lean source)
For a finite time horizon, an event-study system, and a conventional 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 conventional 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 a conventional design, the conventional 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 conventional design, a cohort, and a relative time, the Sun--Abraham contamination weight is that cell's mass times its design residual, divided by the residualized denominator.
Definition (Lean source)
Conventional Sun-Abraham contamination representation. For an event-study system P and conventional design D, if observed outcomes equal the potential outcome under the realized treatment path (consistency), the never-treated potential outcome follows an additive parallel-trends restriction, the residualized displayed-event indicator Rdot is orthogonal in expectation to every function in the event-study nuisance class, the residualized denominator is strictly positive, the coefficient D.mu equals its FWL residualized-ratio form, and the included, displayed, and admissible event times all lie within the declared finite support, then D.mu equals the Sun-Abraham contamination-weighted sum of cohort-relative-time CATTs over every admissible cell.
Formal statement
Proof (Lean source)
For an event-study system P and conventional design D, if observed outcomes equal the potential outcome under the realized treatment path (consistency), the never-treated outcome satisfies additive parallel trends, the design satisfies the finite-cell orthogonality conditions ConventionalResidualization, the residualized denominator is strictly positive, the coefficient D.mu equals its FWL residualized-ratio form, and the included, displayed, and admissible event times all lie within the declared finite support, then D.mu splits as the displayed-event-time contamination term plus the contamination-weighted sum over every other admissible cohort-relative-time cell.
Formal statement
Proof (Lean source)
For an event-study system P and conventional design D, if the consistency, mean-parallel-trends, and no-anticipation causal restrictions hold, the residualized displayed-event indicator Rdot is orthogonal in expectation to every function in the event-study nuisance class, the residualized denominator is strictly positive, the coefficient D.mu equals its FWL residualized-ratio form, and the included, displayed, and admissible event times all lie within the declared finite support, then D.mu equals the contamination-weighted sum of cohort-relative-time CATTs restricted to nonnegative relative times, i.e. once every negative-relative-time CATT vanishes under no-anticipation, the displayed lead's coefficient is a weighted sum of post-treatment effects.
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 the finite-cell residualization and ratio identities for the conventional Sun-Abraham event-study coefficient from a genuine weighted projection on the cohort-by-relative-time cell grid. ★ cellGrid_mu_eq_conventionalMuRatio★ cellGrid_provides_residualization
Sun-Abraham Cell-Grid Projection
This file derives the finite-cell residualization and ratio identities for the conventional Sun-Abraham event-study coefficient from a genuine weighted projection on the cohort-by-relative-time cell grid. 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 conventional 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 conventional 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 conventional 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 conventional 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 conventional 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 conventional 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 conventional design, the cell-grid outcome assigns to each admissible cohort--relative-time cell its observed mean outcome.
Definition (Lean source)
Cell-grid residualization input.
Definition (Lean source)
Cell-grid FWL bridge. Under cell-grid residualization of the event-study design, the conventional event-study coefficient equals the Frisch–Waugh–Lovell residualized ratio computed directly on the cohort × relative-time cell grid.
Formal statement
Proof (Lean source)
For a conventional event-study design D over an event-study system P, if every admissible cohort-relative-time cell has strictly positive population mass, the collection of admissible cells is nonempty, and the design's residualized displayed-event indicator Rdot agrees, cell by cell, with the weighted projection residual on the cell grid, then the three finite-cell orthogonality conditions packaged as ConventionalResidualization — derived here from a genuine weighted projection rather than assumed — hold for D.
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 the public contamination theorems for the conventional Sun-Abraham event-study coefficient. ★ contamination_representation_of_cellGrid★ contamination_representation_split_of_cellGrid★ apparent_pretrends_from_post_treatment_of_cellGrid
Sun-Abraham Contamination Representation
This file provides the public contamination theorems for the conventional Sun-Abraham event-study coefficient. It starts from the cell-grid weighted projection, derives the needed residualization identities, and applies the finite-cell algebra to obtain the displayed contamination formulas.
Contamination representation (genuine). For the conventional event-study coefficient D.mu of a design D on system P, if observed outcomes equal the potential outcome under the realized treatment path (consistency), the never-treated potential outcome follows an additive parallel-trends restriction, the included, displayed, and admissible event times all lie within the declared finite support, and the cell-grid weighted-projection residualization input is supplied, then D.mu equals the Sun-Abraham contamination-weighted sum of cohort-relative-time CATTs over every admissible cell.
Formal statement
Proof (Lean source)
Contamination split (genuine). For the conventional event-study coefficient D.mu of a design D on system P, if the consistency, mean-parallel-trends, and no-anticipation causal restrictions hold, the included, displayed, and admissible event times all lie within the declared finite support, and the cell-grid weighted-projection residualization input is supplied, then D.mu splits as the displayed-event-time contamination term plus the contamination-weighted sum over every other admissible cohort-relative-time cell.
Formal statement
Proof (Lean source)
Apparent pretrends (genuine). For the conventional event-study coefficient D.mu of a design D on system P, if the consistency, mean-parallel-trends, and no-anticipation causal restrictions hold, the included, displayed, and admissible event times all lie within the declared finite event-time support, and the cell-grid weighted-projection residualization input is supplied, then D.mu equals the contamination-weighted sum of cohort-relative-time CATTs restricted to nonnegative relative times — since no-anticipation forces every negative-relative-time CATT to vanish, this exhibits D.mu as a weighted average of post-treatment effects.
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 cohort-cell conditional means and deriving the Sun-Abraham causal restrictions fr ★ toSystem_CATT_eq_po_contrast★ contamination_representation_population★ IW_convex_characterization_population
Sun-Abraham event-study population bridge
This file constructs a finite EventStudySystem from a probability space with
adoption-path potential outcomes, defining its mean fields as cohort-cell
conditional means and deriving the Sun-Abraham 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 conditional mean of on the event that the realized adoption path equals , 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 conditional 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)
Causal-meaning certificate. For a population satisfying the event-study setup, in the system it induces, the treatment-effect estimand at cohort g and relative time e equals the cohort-cell average of the population potential-outcome contrast E[Y_{·t}(g) ∣ G = g] − E[Y_{·t}(∞) ∣ G = g] over the relevant periods, so the estimand carries genuine causal content rather than a free-standing definition on reals.
Formal statement
Proof (Lean source)
Population contamination representation (headline). For a staggered-adoption event-study population E and a conventional design D on the system it induces, if the never-treated potential outcome follows the additive parallel-trends restriction, the included, displayed, and admissible event times all lie within the declared finite support, and the cell-grid weighted-projection residualization input is supplied, then the conventional TWFE event-study coefficient D.mu equals the contamination-weighted sum of genuine population cohort-relative-time effects CATT g e = E[Y_{·t}(g) − Y_{·t}(∞) ∣ G = g]. Consistency and no-anticipation are derived from the potential-outcome structure rather than assumed; this is the Sun-Abraham contamination theorem stated over a genuinely potential-outcome-anchored system.
Formal statement
Proof (Lean source)
Population interaction-weighted characterization (headline). For a staggered-adoption event-study population E and an interaction-weighted design I on the system it induces, if the induced system satisfies comparison-group parallel trends, 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 population CATT at the fixed event time lies between bounds lo and hi, then the interaction-weighted estimand nuIW is the rho-weighted convex average of the genuine population effects CATT g ℓ, and in particular lies between lo and hi — with no contamination from other event times.
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 makes CATT a genuine expected contrast. Under outcome integrability (assumption H5), the two cohort-cell means combine into a single cell mean of the potential-outcome difference: each summand is E[Y_{·t}(g) − Y_{·t}(∞) ∣ G = g], a genuine expectation of the individual treatment-effect random variable. This is where the integrability hypothesis does real work — cellMean_sub requires each slice to be integrable on the cell, so without H5 the two means could not be merged.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]