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.
structure EventStudySystem reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination
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)
parameters
T :
ℕ
fields
Integer-valued period map used to form relative event times.
time :
Fin T → ℤ
Finite adoption cohorts included in the event-study support.
Population share of each adoption path, including `⊤` for never treated.
Balanced cohort-period cell mass.
Factual observed outcome mean by adoption path and period.
Factual observed outcome mean by finite cohort and period.
Mean potential outcome under the cohort's own treatment path.
Mean never-treated potential outcome for each finite cohort.
Mean never-treated potential outcome for any comparison adoption path.
def finitePath reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
A finite adoption path, embedded in WithTop (Fin T).
Definition (Lean source)
def isNeverTreated reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
h = ∞, the never-treated adoption path.
def isEventuallyTreated reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
h < ∞, the path is eventually treated.
def relTime reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Relative event time t - g under the system's integer-valued period map.
Definition (Lean source)
def absorbingTreatment reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Absorbing treatment path 1{h < ∞ and h ≤ t}. Since ⊤ ≤ t is false, the never-treated path is untreated in every finite period.
def targetPeriods reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
The target periods for finite cohort g at relative time e.
Definition (Lean source)
noncomputable def targetPeriods (P : EventStudySystem T) (g : Fin T) (e : ℤ) :
Finset (Fin T) :=
Finset.univ.filter (fun t => P.relTime g t = e)
def baselinePeriods reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Baseline periods with relative time -1 for finite cohort g.
Definition (Lean source)
noncomputable def baselinePeriods (P : EventStudySystem T) (g : Fin T) :
Finset (Fin T) :=
P.targetPeriods g (-1)
def AdmissibleCell reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
A finite cohort-relative-time cell is admissible when the cohort is in support and at least one finite period realizes that relative time.
Definition (Lean source)
def AdmissibleCell (P : EventStudySystem T) (g : Fin T) (e : ℤ) : Prop :=
g ∈ P.cohorts ∧ (P.targetPeriods g e).Nonempty
def admissibleCells reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Finite support of admissible cells, filtered through an explicit finite relative-time support E.
Definition (Lean source)
noncomputable def admissibleCells (P : EventStudySystem T) (E : Finset ℤ) :
Finset (Fin T × ℤ) :=
(P.cohorts.product E).filter (fun ge => P.AdmissibleCell ge.1 ge.2)
def cohortsAtEvent reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Cohorts observed at relative time e, with membership checked against an explicit finite relative-time support.
Definition (Lean source)
noncomputable def cohortsAtEvent (P : EventStudySystem T) (E : Finset ℤ)
(e : ℤ) : Finset (Fin T) :=
P.cohorts.filter (fun g => e ∈ E ∧ P.AdmissibleCell g e)
def cellMassAtEvent reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Balanced finite-cell mass for cohort-relative-time cell (g,e).
Definition (Lean source)
noncomputable def cellMassAtEvent (P : EventStudySystem T) (g : Fin T)
(e : ℤ) : ℝ :=
∑ t ∈ P.targetPeriods g e, P.cellMass g t
def observedCellMean reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Average factual observed outcome over the periods realizing (g,e).
Definition (Lean source)
noncomputable def observedCellMean (P : EventStudySystem T) (g : Fin T)
(e : ℤ) : ℝ :=
((P.targetPeriods g e).card : ℝ)⁻¹ *
∑ t ∈ P.targetPeriods g e, P.observedMean g t
def meanCellContrast reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Average treated-minus-never potential-outcome contrast over (g,e).
Definition (Lean source)
noncomputable def meanCellContrast (P : EventStudySystem T) (g : Fin T)
(e : ℤ) : ℝ :=
((P.targetPeriods g e).card : ℝ)⁻¹ *
∑ t ∈ P.targetPeriods g e, (P.treatedMean g t - P.untreatedMean g t)
def CATT reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Cohort average treatment effect on the treated for the finite cohort-relative-time cell (g,e).
Definition (Lean source)
def pathTargetMean reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Target-period observed mean for an arbitrary adoption path, used by the IW comparison-group DID contrast.
Definition (Lean source)
noncomputable def pathTargetMean (P : EventStudySystem T)
(h : WithTop (Fin T)) (g : Fin T) (e : ℤ) : ℝ :=
((P.targetPeriods g e).card : ℝ)⁻¹ *
∑ t ∈ P.targetPeriods g e, P.observedPathMean h t
def pathBaselineMean reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Baseline observed mean for an arbitrary adoption path, using relative time -1 for treated cohort g.
Definition (Lean source)
noncomputable def pathBaselineMean (P : EventStudySystem T)
(h : WithTop (Fin T)) (g : Fin T) : ℝ :=
((P.baselinePeriods g).card : ℝ)⁻¹ *
∑ t ∈ P.baselinePeriods g, P.observedPathMean h t
def Consistency reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Consistency for observed finite-cohort outcome means.
Definition (Lean source)
def Consistency (P : EventStudySystem T) : Prop :=
∀ g ∈ P.cohorts, ∀ t, P.observedMean g t = P.treatedMean g t
def PathConsistency reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Path-level consistency for comparison-group adoption paths.
Definition (Lean source)
def PathConsistency (P : EventStudySystem T) : Prop :=
∀ (h : WithTop (Fin T)) (t : Fin T),
absorbingTreatment h t = 0 → P.observedPathMean h t = P.untreatedPathMean h t
def NoAnticipation reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
No anticipation in mean potential outcomes.
Definition (Lean source)
def NoAnticipation (P : EventStudySystem T) : Prop :=
∀ g ∈ P.cohorts, ∀ t, P.time t < P.time g →
P.treatedMean g t = P.untreatedMean g t
def MeanParallelUntreated reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Additive mean parallel untreated paths.
Definition (Lean source)
def MeanParallelUntreated (P : EventStudySystem T) : Prop :=
∃ h : Fin T → Fin T → ℝ, IsUnitTimeAdditive h ∧
∀ g ∈ P.cohorts, ∀ t, P.untreatedMean g t = h g t
structure EventStudyCausalRestrictions reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Sun-Abraham event-study causal restrictions. Field names mirror the NL artifact's assumption names.
Definition (Lean source)
parameters
P :
fields
hConsistency :
P.Consistency
hNoAnticipation :
P.NoAnticipation
hMeanParallelUntreated :
P.MeanParallelUntreated
theorem CATT_eq_zero_of_noAnticipation reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
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
hypotheses
conclusion
P.CATT g e = 0
Proof (Lean source)
theorem CATT_eq_zero_of_noAnticipation (P : EventStudySystem T)
(hNoAnticipation : P.NoAnticipation) {g : Fin T} {e : ℤ}
(hg : g ∈ P.cohorts) (he : e < 0) :
P.CATT g e = 0 := by
unfold CATT meanCellContrast
rw [Finset.sum_eq_zero]
· simp
· intro t ht
have hrel : P.relTime g t = e := by
simpa [targetPeriods] using ht
have hpre : P.time t < P.time g := by
have hneg : P.relTime g t < 0 := by
simpa [hrel] using he
simpa [relTime] using (sub_neg.mp hneg)
have hmean := hNoAnticipation g hg t hpre
simp [hmean]
theorem observedCellMean_eq_fixedEffects_add_CATT reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
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
hypotheses
P :
hConsistency :
P.Consistency
hMeanParallelUntreated :
P.MeanParallelUntreated
g :
Fin T
e :
ℤ
hg :
g ∈ P.cohorts
Proof (Lean source)
theorem observedCellMean_eq_fixedEffects_add_CATT (P : EventStudySystem T)
(hConsistency : P.Consistency) (hMeanParallelUntreated : P.MeanParallelUntreated)
{g : Fin T} {e : ℤ}
(hg : g ∈ P.cohorts) :
∃ alpha : Fin T → ℝ, ∃ lambda : Fin T → ℝ,
P.observedCellMean g e =
((P.targetPeriods g e).card : ℝ)⁻¹ *
∑ t ∈ P.targetPeriods g e, (alpha g + lambda t) +
P.CATT g e := by
rcases hMeanParallelUntreated with ⟨hFE, ⟨alpha, lambda, hFE_add⟩, hUntreated⟩
refine ⟨alpha, lambda, ?_⟩
unfold observedCellMean CATT meanCellContrast
have hsum :
(∑ t ∈ P.targetPeriods g e, P.observedMean g t) =
(∑ t ∈ P.targetPeriods g e, (alpha g + lambda t)) +
∑ t ∈ P.targetPeriods g e, (P.treatedMean g t - P.untreatedMean g t) := by
calc
(∑ t ∈ P.targetPeriods g e, P.observedMean g t) =
∑ t ∈ P.targetPeriods g e,
((alpha g + lambda t) + (P.treatedMean g t - P.untreatedMean g t)) := by
apply Finset.sum_congr rfl
intro t ht
rw [hConsistency g hg t, hUntreated g hg t, hFE_add g t]
calc
P.treatedMean g t =
P.treatedMean g t - (alpha g + lambda t) + (alpha g + lambda t) := by
exact (sub_add_cancel (P.treatedMean g t) (alpha g + lambda t)).symm
_ = alpha g + lambda t + (P.treatedMean g t - (alpha g + lambda t)) := by
rw [add_comm]
_ = (∑ t ∈ P.targetPeriods g e, (alpha g + lambda t)) +
∑ t ∈ P.targetPeriods g e, (P.treatedMean g t - P.untreatedMean g t) := by
rw [Finset.sum_add_distrib]
rw [hsum, mul_add]
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.hypothesesconclusionP.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.
def eventIndicator reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Included-event-time indicator on a cohort-relative-time cell.
Definition (Lean source)
noncomputable def eventIndicator (k e : ℤ) : ℝ :=
if e = k then 1 else 0
structure ConventionalDesign reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Conventional event-study finite design for the coefficient on displayedEvent.
Definition (Lean source)
parameters
P :
fields
Finite support of relative times used in the cell expansion.
eventSupport :
Finset ℤ
Included relative-time indicators in the conventional TWFE regression.
includedEvents :
Finset ℤ
Omitted reference relative time.
omittedEvent :
ℤ
Displayed event time `l` whose coefficient is characterized.
displayedEvent :
ℤ
Residualized relative-time indicator `Rdot^l`, constant on cells.
Rdot :
Fin T → ℤ → ℝ
Conventional population TWFE event-study coefficient `mu_l`.
mu :
ℝ
def IsEventStudyNuisance reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Finite-span nuisance class for the coefficient on R^l: cohort effects, period effects, and other included relative-time indicators.
Definition (Lean source)
def IsEventStudyNuisance (P : EventStudySystem T) (D : P.ConventionalDesign)
(h : Fin T → Fin T → ℝ) : Prop :=
∃ hAdd : Fin T → Fin T → ℝ, Causalean.Panel.Weighted.IsUnitTimeAdditive hAdd ∧
∃ gamma : ℤ → ℝ,
∀ g ∈ P.cohorts, ∀ t,
h g t = hAdd g t +
∑ k ∈ D.includedEvents.filter (fun k => k ≠ D.displayedEvent),
gamma k * eventIndicator k (P.relTime g t)
def cellAverage reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Average of a cohort-period nuisance function over the finite periods that realize cell (g,e).
Definition (Lean source)
noncomputable def cellAverage (P : EventStudySystem T)
(h : Fin T → Fin T → ℝ) (g : Fin T) (e : ℤ) : ℝ :=
((P.targetPeriods g e).card : ℝ)⁻¹ *
∑ t ∈ P.targetPeriods g e, h g t
structure ConventionalResidualization reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Finite-cell residualization record for the conventional coefficient.
Definition (Lean source)
parameters
P :
D :
P.ConventionalDesign
fields
hResidualization :
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
hOtherIncludedOrthogonal :
∀ e ∈ D.includedEvents
if
e ≠ D.displayedEvent
then
∑ g ∈ P.cohortsAtEvent D.eventSupport e, P.cellMassAtEvent g e * D.Rdot g e = 0
def residualDenom reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Finite residualized denominator E[Rdot^l R^l].
Definition (Lean source)
noncomputable def residualDenom (P : EventStudySystem T)
(D : P.ConventionalDesign) : ℝ :=
∑ ge ∈ P.admissibleCells D.eventSupport,
P.cellMassAtEvent ge.1 ge.2 * D.Rdot ge.1 ge.2 *
eventIndicator D.displayedEvent ge.2
def residualNumerator reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Finite residualized numerator E[Rdot^l Y].
Definition (Lean source)
noncomputable def residualNumerator (P : EventStudySystem T)
(D : P.ConventionalDesign) : ℝ :=
∑ ge ∈ P.admissibleCells D.eventSupport,
P.cellMassAtEvent ge.1 ge.2 * D.Rdot ge.1 ge.2 *
P.observedCellMean ge.1 ge.2
def conventionalMuRatio reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Residualized-ratio form of the conventional event-study coefficient.
Definition (Lean source)
noncomputable def conventionalMuRatio (P : EventStudySystem T)
(D : P.ConventionalDesign) : ℝ :=
P.residualNumerator D / P.residualDenom D
structure ConventionalFiniteSupport reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
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)
parameters
P :
D :
P.ConventionalDesign
fields
hIncludedInSupport :
∀ e ∈ D.includedEvents, e ∈ D.eventSupport
hDisplayedInSupport :
D.displayedEvent ∈ D.eventSupport
hCellsSupported :
∀ ge ∈ P.admissibleCells D.eventSupport, ge.1 ∈ P.cohorts ∧ ge.2 ∈ D.eventSupport
def omega reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Sun-Abraham contamination weight for the conventional event-study coefficient.
Definition (Lean source)
noncomputable def omega (P : EventStudySystem T) (D : P.ConventionalDesign)
(g : Fin T) (e : ℤ) : ℝ :=
(P.cellMassAtEvent g e * D.Rdot g e) / P.residualDenom D
theorem contamination_representation reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
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
hypotheses
P :
D :
P.ConventionalDesign
hConsistency :
P.Consistency
hMeanParallelUntreated :
P.MeanParallelUntreated
hNuisanceOrthogonal :
hDenomPos :
0 < P.residualDenom D
hMuRatio :
D.mu = P.conventionalMuRatio D
hSupport :
P.ConventionalFiniteSupport D
conclusion
D.mu = ∑ ge ∈ P.admissibleCells D.eventSupport, P.omega D ge.1 ge.2 * P.CATT ge.1 ge.2
Proof (Lean source)
theorem contamination_representation (P : EventStudySystem T)
(D : P.ConventionalDesign)
(hConsistency : P.Consistency)
(hMeanParallelUntreated : P.MeanParallelUntreated)
(hNuisanceOrthogonal :
∀ h : Fin T → Fin T → ℝ, P.IsEventStudyNuisance D h →
∑ ge ∈ P.admissibleCells D.eventSupport,
P.cellMassAtEvent ge.1 ge.2 * D.Rdot ge.1 ge.2 *
P.cellAverage h ge.1 ge.2 = 0)
(hDenomPos : 0 < P.residualDenom D)
(hMuRatio : D.mu = P.conventionalMuRatio D)
(hSupport : P.ConventionalFiniteSupport D) :
D.mu =
∑ ge ∈ P.admissibleCells D.eventSupport,
P.omega D ge.1 ge.2 * P.CATT ge.1 ge.2 := by
have _ : P.residualDenom D ≠ 0 := ne_of_gt hDenomPos
rcases hMeanParallelUntreated with ⟨hAdd, ⟨alpha, lambda, hAdd_eq⟩, hUntreated⟩
let hFE : Fin T → Fin T → ℝ := fun g t => alpha g + lambda t
have hNuisance : P.IsEventStudyNuisance D hFE := by
refine ⟨hFE, ⟨alpha, lambda, ?_⟩, fun _ => 0, ?_⟩
· intro g t
rfl
intro g hg t
simp [hFE]
have hFE_zero :
∑ ge ∈ P.admissibleCells D.eventSupport,
P.cellMassAtEvent ge.1 ge.2 * D.Rdot ge.1 ge.2 *
P.cellAverage hFE ge.1 ge.2 = 0 :=
hNuisanceOrthogonal hFE hNuisance
have hObs :
∀ ge ∈ P.admissibleCells D.eventSupport,
P.observedCellMean ge.1 ge.2 =
P.cellAverage hFE ge.1 ge.2 + P.CATT ge.1 ge.2 := by
intro ge hge
have hg : ge.1 ∈ P.cohorts := (hSupport.hCellsSupported ge hge).1
unfold observedCellMean cellAverage hFE
change
((P.targetPeriods ge.1 ge.2).card : ℝ)⁻¹ *
∑ t ∈ P.targetPeriods ge.1 ge.2, P.observedMean ge.1 t =
((P.targetPeriods ge.1 ge.2).card : ℝ)⁻¹ *
∑ t ∈ P.targetPeriods ge.1 ge.2, (alpha ge.1 + lambda t) +
((P.targetPeriods ge.1 ge.2).card : ℝ)⁻¹ *
∑ t ∈ P.targetPeriods ge.1 ge.2,
(P.treatedMean ge.1 t - P.untreatedMean ge.1 t)
have hsum :
(∑ t ∈ P.targetPeriods ge.1 ge.2, P.observedMean ge.1 t) =
(∑ t ∈ P.targetPeriods ge.1 ge.2, (alpha ge.1 + lambda t)) +
∑ t ∈ P.targetPeriods ge.1 ge.2,
(P.treatedMean ge.1 t - P.untreatedMean ge.1 t) := by
calc
(∑ t ∈ P.targetPeriods ge.1 ge.2, P.observedMean ge.1 t) =
∑ t ∈ P.targetPeriods ge.1 ge.2,
((alpha ge.1 + lambda t) +
(P.treatedMean ge.1 t - P.untreatedMean ge.1 t)) := by
apply Finset.sum_congr rfl
intro t ht
rw [hConsistency ge.1 hg t, hUntreated ge.1 hg t, hAdd_eq ge.1 t]
ring
_ = (∑ t ∈ P.targetPeriods ge.1 ge.2, (alpha ge.1 + lambda t)) +
∑ t ∈ P.targetPeriods ge.1 ge.2,
(P.treatedMean ge.1 t - P.untreatedMean ge.1 t) := by
rw [Finset.sum_add_distrib]
rw [hsum, mul_add]
have hNumerator :
P.residualNumerator D =
∑ ge ∈ P.admissibleCells D.eventSupport,
P.cellMassAtEvent ge.1 ge.2 * D.Rdot ge.1 ge.2 *
P.CATT ge.1 ge.2 := by
unfold residualNumerator
calc
∑ ge ∈ P.admissibleCells D.eventSupport,
P.cellMassAtEvent ge.1 ge.2 * D.Rdot ge.1 ge.2 *
P.observedCellMean ge.1 ge.2 =
∑ ge ∈ P.admissibleCells D.eventSupport,
P.cellMassAtEvent ge.1 ge.2 * D.Rdot ge.1 ge.2 *
(P.cellAverage hFE ge.1 ge.2 + P.CATT ge.1 ge.2) := by
apply Finset.sum_congr rfl
intro ge hge
rw [hObs ge hge]
_ =
(∑ ge ∈ P.admissibleCells D.eventSupport,
P.cellMassAtEvent ge.1 ge.2 * D.Rdot ge.1 ge.2 *
P.cellAverage hFE ge.1 ge.2) +
∑ ge ∈ P.admissibleCells D.eventSupport,
P.cellMassAtEvent ge.1 ge.2 * D.Rdot ge.1 ge.2 *
P.CATT ge.1 ge.2 := by
simp_rw [mul_add]
rw [Finset.sum_add_distrib]
_ =
∑ ge ∈ P.admissibleCells D.eventSupport,
P.cellMassAtEvent ge.1 ge.2 * D.Rdot ge.1 ge.2 *
P.CATT ge.1 ge.2 := by
rw [hFE_zero, zero_add]
calc
D.mu = P.residualNumerator D / P.residualDenom D := hMuRatio
_ =
(∑ ge ∈ P.admissibleCells D.eventSupport,
P.cellMassAtEvent ge.1 ge.2 * D.Rdot ge.1 ge.2 *
P.CATT ge.1 ge.2) / P.residualDenom D := by
rw [hNumerator]
_ =
∑ ge ∈ P.admissibleCells D.eventSupport,
P.omega D ge.1 ge.2 * P.CATT ge.1 ge.2 := by
rw [Finset.sum_div]
apply Finset.sum_congr rfl
intro ge hge
simp [omega]
ring
theorem contamination_representation_split reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
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
hypotheses
P :
D :
P.ConventionalDesign
hConsistency :
P.Consistency
hMeanParallelUntreated :
P.MeanParallelUntreated
hResidualization :
P.ConventionalResidualization D
hDenomPos :
0 < P.residualDenom D
hMuRatio :
D.mu = P.conventionalMuRatio D
hSupport :
P.ConventionalFiniteSupport D
Proof (Lean source)
theorem contamination_representation_split (P : EventStudySystem T)
(D : P.ConventionalDesign)
(hConsistency : P.Consistency)
(hMeanParallelUntreated : P.MeanParallelUntreated)
(hResidualization : P.ConventionalResidualization D)
(hDenomPos : 0 < P.residualDenom D)
(hMuRatio : D.mu = P.conventionalMuRatio D)
(hSupport : P.ConventionalFiniteSupport D) :
D.mu =
(∑ g ∈ P.cohortsAtEvent D.eventSupport D.displayedEvent,
P.omega D g D.displayedEvent * P.CATT g D.displayedEvent) +
(∑ ge ∈ (P.admissibleCells D.eventSupport).filter
(fun ge => ge.2 ≠ D.displayedEvent),
P.omega D ge.1 ge.2 * P.CATT ge.1 ge.2) := by
let F : Fin T × ℤ → ℝ := fun ge => P.omega D ge.1 ge.2 * P.CATT ge.1 ge.2
have hMain :
D.mu = ∑ ge ∈ P.admissibleCells D.eventSupport, F ge := by
simpa [F] using
contamination_representation P D hConsistency
hMeanParallelUntreated hResidualization.hResidualization hDenomPos
hMuRatio hSupport
have hDisplayedCells :
(P.admissibleCells D.eventSupport).filter
(fun ge => ge.2 = D.displayedEvent) =
(P.cohortsAtEvent D.eventSupport D.displayedEvent).map
⟨fun g => (g, D.displayedEvent),
by
intro a b h
exact congrArg Prod.fst h⟩ := by
ext ge
rcases ge with ⟨g, e⟩
simp [admissibleCells, cohortsAtEvent]
constructor
· rintro ⟨⟨⟨hg, heSupport⟩, hAdm⟩, rfl⟩
exact ⟨g, ⟨hg, heSupport, hAdm⟩, rfl⟩
· rintro ⟨a, ⟨hg, hDisplayedSupport, hAdm⟩, hEq⟩
-- `simp` no longer reduces the `Embedding` structure-literal application,
-- so restate the pair equation in reduced form (definitionally equal).
have hEq' : (a, D.displayedEvent) = (g, e) := hEq
have ha : a = g := congrArg Prod.fst hEq'
have he : D.displayedEvent = e := congrArg snd hEq'
subst ha
subst he
exact ⟨⟨⟨hg, hDisplayedSupport⟩, hAdm⟩, rfl⟩
calc
D.mu = ∑ ge ∈ P.admissibleCells D.eventSupport, F ge := hMain
_ =
(∑ ge ∈ (P.admissibleCells D.eventSupport).filter
(fun ge => ge.2 = D.displayedEvent), F ge) +
(∑ ge ∈ (P.admissibleCells D.eventSupport).filter
(fun ge => ge.2 ≠ D.displayedEvent), F ge) := by
exact (Finset.sum_filter_add_sum_filter_not
(P.admissibleCells D.eventSupport)
(fun ge : Fin T × ℤ => ge.2 = D.displayedEvent) F).symm
_ =
(∑ g ∈ P.cohortsAtEvent D.eventSupport D.displayedEvent,
P.omega D g D.displayedEvent * P.CATT g D.displayedEvent) +
(∑ ge ∈ (P.admissibleCells D.eventSupport).filter
(fun ge => ge.2 ≠ D.displayedEvent),
P.omega D ge.1 ge.2 * P.CATT ge.1 ge.2) := by
rw [hDisplayedCells, Finset.sum_map]
rfl
theorem apparent_pretrends_from_post_treatment reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
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
hypotheses
P :
D :
P.ConventionalDesign
hCausal :
P.EventStudyCausalRestrictions
hNuisanceOrthogonal :
hDenomPos :
0 < P.residualDenom D
hMuRatio :
D.mu = P.conventionalMuRatio D
hSupport :
P.ConventionalFiniteSupport D
Proof (Lean source)
theorem apparent_pretrends_from_post_treatment (P : EventStudySystem T)
(D : P.ConventionalDesign)
(hCausal : P.EventStudyCausalRestrictions)
(hNuisanceOrthogonal :
∀ h : Fin T → Fin T → ℝ, P.IsEventStudyNuisance D h →
∑ ge ∈ P.admissibleCells D.eventSupport,
P.cellMassAtEvent ge.1 ge.2 * D.Rdot ge.1 ge.2 *
P.cellAverage h ge.1 ge.2 = 0)
(hDenomPos : 0 < P.residualDenom D)
(hMuRatio : D.mu = P.conventionalMuRatio D)
(hSupport : P.ConventionalFiniteSupport D) :
D.mu =
∑ ge ∈ (P.admissibleCells D.eventSupport).filter (fun ge => 0 ≤ ge.2),
P.omega D ge.1 ge.2 * P.CATT ge.1 ge.2 := by
let F : Fin T × ℤ → ℝ := fun ge => P.omega D ge.1 ge.2 * P.CATT ge.1 ge.2
have hMain :
D.mu = ∑ ge ∈ P.admissibleCells D.eventSupport, F ge := by
simpa [F] using
contamination_representation P D hCausal.hConsistency
hCausal.hMeanParallelUntreated hNuisanceOrthogonal hDenomPos
hMuRatio hSupport
have hNegZero :
∑ ge ∈ (P.admissibleCells D.eventSupport).filter
(fun ge => ¬ 0 ≤ ge.2), F ge = 0 := by
apply Finset.sum_eq_zero
intro ge hge
have hmem : ge ∈ P.admissibleCells D.eventSupport := (Finset.mem_filter.mp hge).1
have hneg : ¬ 0 ≤ ge.2 := (Finset.mem_filter.mp hge).2
have hlt : ge.2 < 0 := not_le.mp hneg
have hg : ge.1 ∈ P.cohorts := (hSupport.hCellsSupported ge hmem).1
simp [F, P.CATT_eq_zero_of_noAnticipation hCausal.hNoAnticipation hg hlt]
calc
D.mu = ∑ ge ∈ P.admissibleCells D.eventSupport, F ge := hMain
_ =
(∑ ge ∈ (P.admissibleCells D.eventSupport).filter
(fun ge => 0 ≤ ge.2), F ge) +
(∑ ge ∈ (P.admissibleCells D.eventSupport).filter
(fun ge => ¬ 0 ≤ ge.2), F ge) := by
exact (Finset.sum_filter_add_sum_filter_not
(P.admissibleCells D.eventSupport)
(fun ge : Fin T × ℤ => 0 ≤ ge.2) F).symm
_ = ∑ ge ∈ (P.admissibleCells D.eventSupport).filter
(fun ge => 0 ≤ ge.2), F ge := by
rw [hNegZero, add_zero]
2 supporting declarations (lemmas, instances)
-
desired_event_weights_sum_onetheorem — Desired-event-time weights sum to one.hypothesesP :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.hypothesesP :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.
abbrev CellIndex reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
The finite cell index type for the conventional design D: the admissible cohort-relative-time cells.
Definition (Lean source)
abbrev CellIndex (P : EventStudySystem T) (D : P.ConventionalDesign) : Type :=
{ge : Fin T × ℤ // ge ∈ P.admissibleCells D.eventSupport}
def cellTotalMass reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Total admissible cell mass Z = Σ_{(g,e)} cellMassAtEvent g e.
Definition (Lean source)
noncomputable def cellTotalMass (P : EventStudySystem T) (D : P.ConventionalDesign) : ℝ :=
∑ ge ∈ P.admissibleCells D.eventSupport, P.cellMassAtEvent ge.1 ge.2
def cellSupport reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
The cell-grid weighted support: the empirical population over admissible cells with weight cellMassAtEvent / Z.
Definition (Lean source)
noncomputable def 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) :
WeightedSupport (P.CellIndex D) where
observed := Finset.univ
observed_nonempty := by
classical
rw [Finset.univ_nonempty_iff]
obtain ⟨ge, hge⟩ := hne
exact ⟨⟨ge, hge⟩⟩
weight := fun cell => P.cellMassAtEvent cell.val.1 cell.val.2 / P.cellTotalMass D
weight_pos := by
intro cell _
have hZ : 0 < P.cellTotalMass D :=
Finset.sum_pos (fun ge hge => hpos ge hge) hne
exact div_pos (hpos cell.val cell.property) hZ
weight_zero_off := by
intro cell hcell
exact absurd (Finset.mem_univ cell) hcell
weight_sum_one := by
classical
have hZ : 0 < P.cellTotalMass D :=
Finset.sum_pos (fun ge hge => hpos ge hge) hne
have hsum :
∑ cell : P.CellIndex D,
P.cellMassAtEvent cell.val.1 cell.val.2 / P.cellTotalMass D =
(∑ cell : P.CellIndex D,
P.cellMassAtEvent cell.val.1 cell.val.2) / P.cellTotalMass D := by
rw [← Finset.sum_div]
rw [show (Finset.univ : Finset (P.CellIndex D)) = Finset.univ from rfl, hsum]
rw [Finset.sum_coe_sort (P.admissibleCells D.eventSupport)
(fun ge => P.cellMassAtEvent ge.1 ge.2)]
rw [← cellTotalMass]
exact div_self hZ.ne'
def cellNuisanceGen reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Generators of the cell-nuisance subspace: cell-evaluated event-study nuisance functions.
Definition (Lean source)
def cellNuisanceGen (P : EventStudySystem T) (D : P.ConventionalDesign) :
Set (P.CellIndex D → ℝ) :=
{f | ∃ hCell : Fin T → Fin T → ℝ, P.IsEventStudyNuisance D hCell ∧
f = fun cell => P.cellAverage hCell cell.val.1 cell.val.2}
def cellNuisance reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
The cell-nuisance subspace H on the cell grid: the span of cell-evaluated event-study nuisance functions.
Definition (Lean source)
noncomputable def cellNuisance (P : EventStudySystem T) (D : P.ConventionalDesign) :
Submodule ℝ (P.CellIndex D → ℝ) :=
span ℝ (P.cellNuisanceGen D)
def cellRegressor reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Cell-grid regressor: the displayed-event relative-time indicator as a cell function.
Definition (Lean source)
noncomputable def cellRegressor (P : EventStudySystem T) (D : P.ConventionalDesign) :
P.CellIndex D → ℝ :=
fun cell => eventIndicator D.displayedEvent cell.val.2
def cellOutcome reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Cell-grid outcome: the observed cell mean as a cell function.
Definition (Lean source)
noncomputable def cellOutcome (P : EventStudySystem T) (D : P.ConventionalDesign) :
P.CellIndex D → ℝ :=
fun cell => P.observedCellMean cell.val.1 cell.val.2
structure CellGridResidualization reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Cell-grid residualization input.
Definition (Lean source)
parameters
P :
D :
P.ConventionalDesign
fields
hCellMassPos :
∀ ge ∈ P.admissibleCells D.eventSupport, 0 < P.cellMassAtEvent ge.1 ge.2
hCellNonempty :
(P.admissibleCells D.eventSupport).Nonempty
hDenomPos :
0 < P.residualDenom D
hRdotResidual :
∀ cell : P.CellIndex D,
D.Rdot cell.val.1 cell.val.2
= (P.cellSupport D hCellMassPos hCellNonempty).tildeX (P.cellNuisance D) (P.cellRegressor D) cell
hMuNormalEqs :
theorem cellGrid_mu_eq_conventionalMuRatio reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
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
hypotheses
h :
P.CellGridResidualization D
conclusion
D.mu = P.conventionalMuRatio D
Proof (Lean source)
theorem cellGrid_mu_eq_conventionalMuRatio (h : P.CellGridResidualization D) :
D.mu = P.conventionalMuRatio D := by
classical
have hZpos : 0 < P.cellTotalMass D :=
Finset.sum_pos (fun ge hge => h.hCellMassPos ge hge) h.hCellNonempty
have hZ : P.cellTotalMass D ≠ 0 := hZpos.ne'
have hRdot := tildeX_eq_Rdot h
have hnum :
(P.cellSupport D h.hCellMassPos h.hCellNonempty).ip
((P.cellSupport D h.hCellMassPos h.hCellNonempty).tildeX (P.cellNuisance D)
(P.cellRegressor D))
(P.cellOutcome D)
= P.residualNumerator D / P.cellTotalMass D := by
rw [hRdot]
exact P.ip_cellSupport D h.hCellMassPos h.hCellNonempty
(fun ge => D.Rdot ge.1 ge.2) (fun ge => P.observedCellMean ge.1 ge.2)
have hden :
(P.cellSupport D h.hCellMassPos h.hCellNonempty).ip
((P.cellSupport D h.hCellMassPos h.hCellNonempty).tildeX (P.cellNuisance D)
(P.cellRegressor D))
((P.cellSupport D h.hCellMassPos h.hCellNonempty).tildeX (P.cellNuisance D)
(P.cellRegressor D))
= P.residualDenom D / P.cellTotalMass D := by
rw [← (P.cellSupport D h.hCellMassPos h.hCellNonempty).ip_tildeX_self
(P.cellNuisance D) (P.cellRegressor D), hRdot]
exact P.ip_cellSupport D h.hCellMassPos h.hCellNonempty
(fun ge => D.Rdot ge.1 ge.2) (fun ge => eventIndicator D.displayedEvent ge.2)
have hpos_ip :
0 < (P.cellSupport D h.hCellMassPos h.hCellNonempty).ip
((P.cellSupport D h.hCellMassPos h.hCellNonempty).tildeX (P.cellNuisance D)
(P.cellRegressor D))
((P.cellSupport D h.hCellMassPos h.hCellNonempty).tildeX (P.cellNuisance D)
(P.cellRegressor D)) := by
rw [hden]; exact div_pos h.hDenomPos hZpos
obtain ⟨α, hα_mem, hNR, hNH⟩ := h.hMuNormalEqs
have hmu := (P.cellSupport D h.hCellMassPos h.hCellNonempty).scalar_fwl_of_normalEqs
(P.cellNuisance D) (P.cellRegressor D) (P.cellOutcome D) D.mu α
hα_mem hpos_ip.ne' hNR hNH
rw [hmu, hnum, hden, EventStudySystem.conventionalMuRatio]
have hDen : P.residualDenom D ≠ 0 := h.hDenomPos.ne'
field_simp
theorem cellGrid_provides_residualization reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
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
hypotheses
hCellMassPos :
∀ ge ∈ P.admissibleCells D.eventSupport, 0 < P.cellMassAtEvent ge.1 ge.2
hCellNonempty :
(P.admissibleCells D.eventSupport).Nonempty
hRdotResidual :
∀ cell : P.CellIndex D,
D.Rdot cell.val.1 cell.val.2
= (P.cellSupport D hCellMassPos hCellNonempty).tildeX (P.cellNuisance D) (P.cellRegressor D) cell
conclusion
P.ConventionalResidualization D
Proof (Lean source)
theorem cellGrid_provides_residualization
(hCellMassPos : ∀ ge ∈ P.admissibleCells D.eventSupport,
0 < P.cellMassAtEvent ge.1 ge.2)
(hCellNonempty : (P.admissibleCells D.eventSupport).Nonempty)
(hRdotResidual : ∀ cell : P.CellIndex D,
D.Rdot cell.val.1 cell.val.2
= (P.cellSupport D hCellMassPos hCellNonempty).tildeX (P.cellNuisance D)
(P.cellRegressor D) cell) :
P.ConventionalResidualization D := by
classical
have hZpos : 0 < P.cellTotalMass D :=
Finset.sum_pos (fun ge hge => hCellMassPos ge hge) hCellNonempty
have hZ : P.cellTotalMass D ≠ 0 := hZpos.ne'
have hRdot :
(P.cellSupport D hCellMassPos hCellNonempty).tildeX (P.cellNuisance D)
(P.cellRegressor D) = fun cell => D.Rdot cell.val.1 cell.val.2 := by
funext cell
exact (hRdotResidual cell).symm
refine ⟨?_, ?_, ?_⟩
· -- hResidualization
intro hCell hN
have hmem := P.cellAverage_mem_cellNuisance D hN
have hortho := (P.cellSupport D hCellMassPos hCellNonempty).residualize_in_orthogonal
(P.cellNuisance D) (P.cellRegressor D) hmem
rw [hRdot] at hortho
have hip :
(P.cellSupport D hCellMassPos hCellNonempty).ip
(fun cell => D.Rdot cell.val.1 cell.val.2)
(fun cell => P.cellAverage hCell cell.val.1 cell.val.2)
= (∑ ge ∈ P.admissibleCells D.eventSupport,
P.cellMassAtEvent ge.1 ge.2 * D.Rdot ge.1 ge.2
* P.cellAverage hCell ge.1 ge.2) / P.cellTotalMass D :=
P.ip_cellSupport D hCellMassPos hCellNonempty
(fun ge => D.Rdot ge.1 ge.2) (fun ge => P.cellAverage hCell ge.1 ge.2)
rw [hip] at hortho
exact (div_eq_zero_iff.mp hortho).resolve_right hZ
· -- hDisplayedExpansion
exact P.sum_admissible_mul_eventIndicator D D.displayedEvent
(fun g e => P.cellMassAtEvent g e * D.Rdot g e)
· -- hOtherIncludedOrthogonal
intro e he_inc he_ne
have hmem := P.eventIndicator_mem_cellNuisance D he_inc he_ne
have hortho := (P.cellSupport D hCellMassPos hCellNonempty).residualize_in_orthogonal
(P.cellNuisance D) (P.cellRegressor D) hmem
rw [hRdot] at hortho
have hip :
(P.cellSupport D hCellMassPos hCellNonempty).ip
(fun cell => D.Rdot cell.val.1 cell.val.2)
(fun cell => eventIndicator e cell.val.2)
= (∑ ge ∈ P.admissibleCells D.eventSupport,
P.cellMassAtEvent ge.1 ge.2 * D.Rdot ge.1 ge.2
* eventIndicator e ge.2) / P.cellTotalMass D :=
P.ip_cellSupport D hCellMassPos hCellNonempty
(fun ge => D.Rdot ge.1 ge.2) (fun ge => eventIndicator e ge.2)
rw [hip] at hortho
have hsum0 :
∑ ge ∈ P.admissibleCells D.eventSupport,
P.cellMassAtEvent ge.1 ge.2 * D.Rdot ge.1 ge.2 * eventIndicator e ge.2 = 0 :=
(div_eq_zero_iff.mp hortho).resolve_right hZ
rw [← P.sum_admissible_mul_eventIndicator D e
(fun g e0 => P.cellMassAtEvent g e0 * D.Rdot g e0)]
exact hsum0
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.hypothesesP :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).hypothesesP :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.hypothesesh :P.CellGridResidualization D
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.
structure IWDesign reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Interaction-weighted finite DID design for a fixed event time.
Definition (Lean source)
parameters
P :
def observedTargetMean reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Observed treated-cohort target mean from the finite-cohort factual means.
Definition (Lean source)
noncomputable def observedTargetMean (P : EventStudySystem T)
(I : P.IWDesign) (g : Fin T) : ℝ :=
((P.targetPeriods g I.eventTime).card : ℝ)⁻¹ *
∑ t ∈ P.targetPeriods g I.eventTime, P.observedMean g t
def observedBaselineMean reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Observed treated-cohort baseline mean from the finite-cohort factual means, using relative time -1.
Definition (Lean source)
noncomputable def observedBaselineMean (P : EventStudySystem T)
(g : Fin T) : ℝ :=
((P.baselinePeriods g).card : ℝ)⁻¹ *
∑ t ∈ P.baselinePeriods g, P.observedMean g t
def comparisonMass reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Total comparison-group population mass for cohort g's IW contrast.
Definition (Lean source)
noncomputable def comparisonMass (P : EventStudySystem T)
(I : P.IWDesign) (g : Fin T) : ℝ :=
∑ h ∈ I.comparisonGroup g, P.cohortShare h
def comparisonMeanChange reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Population-share weighted comparison-group mean change from baseline g-1 to target g+l.
Definition (Lean source)
noncomputable def comparisonMeanChange (P : EventStudySystem T)
(I : P.IWDesign) (g : Fin T) : ℝ :=
(P.comparisonMass I g)⁻¹ *
∑ h ∈ I.comparisonGroup g,
P.cohortShare h * (P.pathTargetMean h g I.eventTime - P.pathBaselineMean h g)
def DIDContrast reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Cohort-specific DID contrast using the treated cohort and its comparison group.
Definition (Lean source)
noncomputable def DIDContrast (P : EventStudySystem T)
(I : P.IWDesign) (g : Fin T) : ℝ :=
(P.observedTargetMean I g - P.observedBaselineMean g) -
P.comparisonMeanChange I g
def Delta reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Cohort-specific IW DID contrast Delta(g,l). It is definitional rather than stored separately, so the IW theorem identifies the actual DID contrast.
Definition (Lean source)
noncomputable def Delta (P : EventStudySystem T) (I : P.IWDesign)
(g : Fin T) : ℝ :=
P.DIDContrast I g
def nuIW reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Interaction-weighted event-study estimand.
Definition (Lean source)
noncomputable def nuIW (P : EventStudySystem T) (I : P.IWDesign) : ℝ :=
∑ g ∈ I.cohortsIW, I.rho g * P.Delta I g
structure IWSupport reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
IW support restrictions for eligible cohorts and their comparison groups.
Definition (Lean source)
parameters
P :
I :
P.IWDesign
fields
hBaselineValid :
∀ g ∈ I.cohortsIW, (P.baselinePeriods g).Nonempty
hTargetValid :
∀ g ∈ I.cohortsIW, g ∈ P.cohorts ∧ (P.targetPeriods g I.eventTime).Nonempty
hCohortSharePos :
∀ g ∈ I.cohortsIW, 0 < P.cohortShare (finitePath g)
hComparisonNonempty :
∀ g ∈ I.cohortsIW, (I.comparisonGroup g).Nonempty
hComparisonPositive :
∀ g ∈ I.cohortsIW, 0 < P.comparisonMass I g
hComparisonUntreatedBaseline :
∀ g ∈ I.cohortsIW,
∀ h ∈ I.comparisonGroup g, ∀ t ∈ P.baselinePeriods g, absorbingTreatment h t = 0
hComparisonUntreatedTarget :
∀ g ∈ I.cohortsIW,
∀ h ∈ I.comparisonGroup g, ∀ t ∈ P.targetPeriods g I.eventTime, absorbingTreatment h t = 0
structure IWComparisonParallelTrends reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
Comparison-group parallel trends for the IW DID contrast.
Definition (Lean source)
parameters
P :
I :
P.IWDesign
fields
hComparisonPositive :
∀ g ∈ I.cohortsIW, 0 < P.comparisonMass I g
hComparisonUntreated :
∀ g ∈ I.cohortsIW,
∀ h ∈ I.comparisonGroup g,
(∀ t ∈ P.baselinePeriods g, absorbingTreatment h t = 0) ∧
(∀ t ∈ P.targetPeriods g I.eventTime, absorbingTreatment h t = 0)
hComparisonParallelTrends :
∀ g ∈ I.cohortsIW,
((P.targetPeriods g I.eventTime).card : ℝ)⁻¹ * ∑ t ∈ P.targetPeriods g I.eventTime, (P.untreatedMean g t)
- ((P.baselinePeriods g).card : ℝ)⁻¹ * ∑ t ∈ P.baselinePeriods g, (P.untreatedMean g t)
= (P.comparisonMass I g)⁻¹ * ∑ h ∈ I.comparisonGroup g, P.cohortShare h * (((P.targetPeriods g I.eventTime).card : ℝ)⁻¹ * ∑ t ∈ P.targetPeriods g I.eventTime, P.untreatedPathMean h t - ((P.baselinePeriods g).card : ℝ)⁻¹ * ∑ t ∈ P.baselinePeriods g, P.untreatedPathMean h t)
theorem IW_Delta_eq_CATT reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
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
hypotheses
P :
I :
P.IWDesign
hConsistency :
P.Consistency
hNoAnticipation :
P.NoAnticipation
hPathConsistency :
P.PathConsistency
hComparisonParallelTrends :
∀ g ∈ I.cohortsIW,
((P.targetPeriods g I.eventTime).card : ℝ)⁻¹ * ∑ t ∈ P.targetPeriods g I.eventTime, (P.untreatedMean g t)
- ((P.baselinePeriods g).card : ℝ)⁻¹ * ∑ t ∈ P.baselinePeriods g, (P.untreatedMean g t)
= (P.comparisonMass I g)⁻¹ * ∑ h ∈ I.comparisonGroup g, P.cohortShare h * (((P.targetPeriods g I.eventTime).card : ℝ)⁻¹ * ∑ t ∈ P.targetPeriods g I.eventTime, P.untreatedPathMean h t - ((P.baselinePeriods g).card : ℝ)⁻¹ * ∑ t ∈ P.baselinePeriods g, P.untreatedPathMean h t)
hCohort :
∀ g ∈ I.cohortsIW, g ∈ P.cohorts
hComparisonUntreatedBaseline :
∀ g ∈ I.cohortsIW,
∀ h ∈ I.comparisonGroup g, ∀ t ∈ P.baselinePeriods g, absorbingTreatment h t = 0
hComparisonUntreatedTarget :
∀ g ∈ I.cohortsIW,
∀ h ∈ I.comparisonGroup g, ∀ t ∈ P.targetPeriods g I.eventTime, absorbingTreatment h t = 0
g :
Fin T
hg :
g ∈ I.cohortsIW
conclusion
P.Delta I g = P.CATT g I.eventTime
Proof (Lean source)
theorem IW_Delta_eq_CATT (P : EventStudySystem T) (I : P.IWDesign)
(hConsistency : P.Consistency)
(hNoAnticipation : P.NoAnticipation)
(hPathConsistency : P.PathConsistency)
(hComparisonParallelTrends : ∀ g ∈ I.cohortsIW,
((P.targetPeriods g I.eventTime).card : ℝ)⁻¹ *
∑ t ∈ P.targetPeriods g I.eventTime,
(P.untreatedMean g t) -
((P.baselinePeriods g).card : ℝ)⁻¹ *
∑ t ∈ P.baselinePeriods g, (P.untreatedMean g t)
=
(P.comparisonMass I g)⁻¹ *
∑ h ∈ I.comparisonGroup g,
P.cohortShare h *
(((P.targetPeriods g I.eventTime).card : ℝ)⁻¹ *
∑ t ∈ P.targetPeriods g I.eventTime, P.untreatedPathMean h t -
((P.baselinePeriods g).card : ℝ)⁻¹ *
∑ t ∈ P.baselinePeriods g, P.untreatedPathMean h t))
(hCohort : ∀ g ∈ I.cohortsIW, g ∈ P.cohorts)
(hComparisonUntreatedBaseline :
∀ g ∈ I.cohortsIW, ∀ h ∈ I.comparisonGroup g,
∀ t ∈ P.baselinePeriods g, absorbingTreatment h t = 0)
(hComparisonUntreatedTarget :
∀ g ∈ I.cohortsIW, ∀ h ∈ I.comparisonGroup g,
∀ t ∈ P.targetPeriods g I.eventTime, absorbingTreatment h t = 0)
{g : Fin T} (hg : g ∈ I.cohortsIW) :
P.Delta I g = P.CATT g I.eventTime := by
have hgCohort : g ∈ P.cohorts := hCohort g hg
have hObsTarget :
P.observedTargetMean I g =
((P.targetPeriods g I.eventTime).card : ℝ)⁻¹ *
∑ t ∈ P.targetPeriods g I.eventTime, P.treatedMean g t := by
unfold observedTargetMean
have hsum :
(∑ t ∈ P.targetPeriods g I.eventTime, P.observedMean g t) =
∑ t ∈ P.targetPeriods g I.eventTime, P.treatedMean g t := by
apply Finset.sum_congr rfl
intro t ht
exact hConsistency g hgCohort t
rw [hsum]
have hObsBaseline :
P.observedBaselineMean g =
((P.baselinePeriods g).card : ℝ)⁻¹ *
∑ t ∈ P.baselinePeriods g, P.untreatedMean g t := by
unfold observedBaselineMean
have hsum :
(∑ t ∈ P.baselinePeriods g, P.observedMean g t) =
∑ t ∈ P.baselinePeriods g, P.untreatedMean g t := by
apply Finset.sum_congr rfl
intro t ht
have hrel : P.relTime g t = -1 := by
simpa [baselinePeriods, targetPeriods] using ht
have hpre : P.time t < P.time g := by
have hneg : P.relTime g t < 0 := by
rw [hrel]
norm_num
simpa [relTime] using (sub_neg.mp hneg)
rw [hConsistency g hgCohort t, hNoAnticipation g hgCohort t hpre]
rw [hsum]
have hPathTarget : ∀ h ∈ I.comparisonGroup g,
P.pathTargetMean h g I.eventTime =
((P.targetPeriods g I.eventTime).card : ℝ)⁻¹ *
∑ t ∈ P.targetPeriods g I.eventTime, P.untreatedPathMean h t := by
intro h hh
unfold pathTargetMean
have hsum :
(∑ t ∈ P.targetPeriods g I.eventTime, P.observedPathMean h t) =
∑ t ∈ P.targetPeriods g I.eventTime, P.untreatedPathMean h t := by
apply Finset.sum_congr rfl
intro t ht
exact P.pathConsistency_observed_eq_untreated hPathConsistency
(hComparisonUntreatedTarget g hg h hh t ht)
rw [hsum]
have hPathBaseline : ∀ h ∈ I.comparisonGroup g,
P.pathBaselineMean h g =
((P.baselinePeriods g).card : ℝ)⁻¹ *
∑ t ∈ P.baselinePeriods g, P.untreatedPathMean h t := by
intro h hh
unfold pathBaselineMean
have hsum :
(∑ t ∈ P.baselinePeriods g, P.observedPathMean h t) =
∑ t ∈ P.baselinePeriods g, P.untreatedPathMean h t := by
apply Finset.sum_congr rfl
intro t ht
exact P.pathConsistency_observed_eq_untreated hPathConsistency
(hComparisonUntreatedBaseline g hg h hh t ht)
rw [hsum]
have hComparison :
P.comparisonMeanChange I g =
(P.comparisonMass I g)⁻¹ *
∑ h ∈ I.comparisonGroup g,
P.cohortShare h *
(((P.targetPeriods g I.eventTime).card : ℝ)⁻¹ *
∑ t ∈ P.targetPeriods g I.eventTime, P.untreatedPathMean h t -
((P.baselinePeriods g).card : ℝ)⁻¹ *
∑ t ∈ P.baselinePeriods g, P.untreatedPathMean h t) := by
unfold comparisonMeanChange
have hsum :
(∑ h ∈ I.comparisonGroup g,
P.cohortShare h *
(P.pathTargetMean h g I.eventTime - P.pathBaselineMean h g)) =
∑ h ∈ I.comparisonGroup g,
P.cohortShare h *
(((P.targetPeriods g I.eventTime).card : ℝ)⁻¹ *
∑ t ∈ P.targetPeriods g I.eventTime, P.untreatedPathMean h t -
((P.baselinePeriods g).card : ℝ)⁻¹ *
∑ t ∈ P.baselinePeriods g, P.untreatedPathMean h t) := by
apply Finset.sum_congr rfl
intro h hh
rw [hPathTarget h hh, hPathBaseline h hh]
rw [hsum]
have hParallel := hComparisonParallelTrends g hg
unfold Delta DIDContrast CATT meanCellContrast
rw [hObsTarget, hObsBaseline, hComparison, ← hParallel]
rw [Finset.sum_sub_distrib]
rw [mul_sub]
rw [sub_sub_sub_cancel_right]
theorem IW_convex_characterization reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
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
hypotheses
P :
I :
P.IWDesign
hConsistency :
P.Consistency
hNoAnticipation :
P.NoAnticipation
hPathConsistency :
P.PathConsistency
hComparisonParallelTrends :
∀ g ∈ I.cohortsIW,
((P.targetPeriods g I.eventTime).card : ℝ)⁻¹ * ∑ t ∈ P.targetPeriods g I.eventTime, P.untreatedMean g t
- ((P.baselinePeriods g).card : ℝ)⁻¹ * ∑ t ∈ P.baselinePeriods g, P.untreatedMean g t
= (P.comparisonMass I g)⁻¹ * ∑ h ∈ I.comparisonGroup g, P.cohortShare h * (((P.targetPeriods g I.eventTime).card : ℝ)⁻¹ * ∑ t ∈ P.targetPeriods g I.eventTime, P.untreatedPathMean h t - ((P.baselinePeriods g).card : ℝ)⁻¹ * ∑ t ∈ P.baselinePeriods g, P.untreatedPathMean h t)
hSupport :
P.IWSupport I
hRhoNonneg :
∀ g ∈ I.cohortsIW, 0 ≤ I.rho g
hRhoSumOne :
∑ g ∈ I.cohortsIW, I.rho g = 1
lo hi :
ℝ
hLo :
∀ g ∈ I.cohortsIW, lo ≤ P.CATT g I.eventTime
hHi :
∀ g ∈ I.cohortsIW, P.CATT g I.eventTime ≤ hi
conclusion
(∀ g ∈ I.cohortsIW, P.Delta I g = P.CATT g I.eventTime) ∧
P.nuIW I = ∑ g ∈ I.cohortsIW, I.rho g * P.CATT g I.eventTime ∧
lo ≤ P.nuIW I ∧
P.nuIW I ≤ hi
Proof (Lean source)
theorem IW_convex_characterization (P : EventStudySystem T) (I : P.IWDesign)
(hConsistency : P.Consistency)
(hNoAnticipation : P.NoAnticipation)
(hPathConsistency : P.PathConsistency)
(hComparisonParallelTrends : ∀ g ∈ I.cohortsIW,
((P.targetPeriods g I.eventTime).card : ℝ)⁻¹ *
∑ t ∈ P.targetPeriods g I.eventTime,
P.untreatedMean g t -
((P.baselinePeriods g).card : ℝ)⁻¹ *
∑ t ∈ P.baselinePeriods g, P.untreatedMean g t
=
(P.comparisonMass I g)⁻¹ *
∑ h ∈ I.comparisonGroup g,
P.cohortShare h *
(((P.targetPeriods g I.eventTime).card : ℝ)⁻¹ *
∑ t ∈ P.targetPeriods g I.eventTime, P.untreatedPathMean h t -
((P.baselinePeriods g).card : ℝ)⁻¹ *
∑ t ∈ P.baselinePeriods g, P.untreatedPathMean h t))
(hSupport : P.IWSupport I)
(hRhoNonneg : ∀ g ∈ I.cohortsIW, 0 ≤ I.rho g)
(hRhoSumOne : ∑ g ∈ I.cohortsIW, I.rho g = 1)
{lo hi : ℝ}
(hLo : ∀ g ∈ I.cohortsIW, lo ≤ P.CATT g I.eventTime)
(hHi : ∀ g ∈ I.cohortsIW, P.CATT g I.eventTime ≤ hi) :
(∀ g ∈ I.cohortsIW, P.Delta I g = P.CATT g I.eventTime) ∧
P.nuIW I = ∑ g ∈ I.cohortsIW, I.rho g * P.CATT g I.eventTime ∧
lo ≤ P.nuIW I ∧ P.nuIW I ≤ hi := by
have hDelta : ∀ g ∈ I.cohortsIW, P.Delta I g = P.CATT g I.eventTime := by
intro g hg
exact P.IW_Delta_eq_CATT I hConsistency hNoAnticipation hPathConsistency
hComparisonParallelTrends
(fun g hg => (hSupport.hTargetValid g hg).1)
hSupport.hComparisonUntreatedBaseline hSupport.hComparisonUntreatedTarget hg
have hAgg : P.nuIW I = ∑ g ∈ I.cohortsIW, I.rho g * P.CATT g I.eventTime := by
unfold nuIW
apply Finset.sum_congr rfl
intro g hg
rw [hDelta g hg]
refine ⟨hDelta, hAgg, ?_, ?_⟩ <;>
rw [hAgg]
· exact (sum_convex_mem_Icc I.cohortsIW I.rho
(fun g => P.CATT g I.eventTime) hRhoNonneg hRhoSumOne hLo hHi).1
· exact (sum_convex_mem_Icc I.cohortsIW I.rho
(fun g => P.CATT g I.eventTime) hRhoNonneg hRhoSumOne hLo hHi).2
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 ≤ hiconclusionlo ≤ ∑ i ∈ s, w i * f i ∧ ∑ 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.
theorem contamination_representation_of_cellGrid reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
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
hypotheses
hConsistency :
P.Consistency
hMeanParallelUntreated :
P.MeanParallelUntreated
hSupport :
P.ConventionalFiniteSupport D
hCell :
P.CellGridResidualization D
conclusion
D.mu = ∑ ge ∈ P.admissibleCells D.eventSupport, P.omega D ge.1 ge.2 * P.CATT ge.1 ge.2
Proof (Lean source)
theorem contamination_representation_of_cellGrid
(hConsistency : P.Consistency) (hMeanParallelUntreated : P.MeanParallelUntreated)
(hSupport : P.ConventionalFiniteSupport D)
(hCell : P.CellGridResidualization D) :
D.mu =
∑ ge ∈ P.admissibleCells D.eventSupport,
P.omega D ge.1 ge.2 * P.CATT ge.1 ge.2 :=
P.contamination_representation D hConsistency hMeanParallelUntreated
(cellGrid_provides_residualization hCell.hCellMassPos hCell.hCellNonempty hCell.hRdotResidual).hResidualization
hCell.hDenomPos (cellGrid_mu_eq_conventionalMuRatio hCell) hSupport
theorem contamination_representation_split_of_cellGrid reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
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
hypotheses
hCausal :
P.EventStudyCausalRestrictions
hSupport :
P.ConventionalFiniteSupport D
hCell :
P.CellGridResidualization D
Proof (Lean source)
theorem contamination_representation_split_of_cellGrid
(hCausal : P.EventStudyCausalRestrictions)
(hSupport : P.ConventionalFiniteSupport D)
(hCell : P.CellGridResidualization D) :
D.mu =
(∑ g ∈ P.cohortsAtEvent D.eventSupport D.displayedEvent,
P.omega D g D.displayedEvent * P.CATT g D.displayedEvent) +
(∑ ge ∈ (P.admissibleCells D.eventSupport).filter
(fun ge => ge.2 ≠ D.displayedEvent),
P.omega D ge.1 ge.2 * P.CATT ge.1 ge.2) :=
P.contamination_representation_split D hCausal.hConsistency hCausal.hMeanParallelUntreated
(cellGrid_provides_residualization hCell.hCellMassPos hCell.hCellNonempty hCell.hRdotResidual)
hCell.hDenomPos (cellGrid_mu_eq_conventionalMuRatio hCell) hSupport
theorem apparent_pretrends_from_post_treatment_of_cellGrid reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudySystem
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)
theorem apparent_pretrends_from_post_treatment_of_cellGrid
(hCausal : P.EventStudyCausalRestrictions)
(hSupport : P.ConventionalFiniteSupport D)
(hCell : P.CellGridResidualization D) :
D.mu =
∑ ge ∈ (P.admissibleCells D.eventSupport).filter (fun ge => 0 ≤ ge.2),
P.omega D ge.1 ge.2 * P.CATT ge.1 ge.2 :=
P.apparent_pretrends_from_post_treatment D hCausal
(cellGrid_provides_residualization hCell.hCellMassPos hCell.hCellNonempty hCell.hRdotResidual).hResidualization
hCell.hDenomPos (cellGrid_mu_eq_conventionalMuRatio hCell) hSupport
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.
structure EventStudyPopulation reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination
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)
parameters
T :
ℕ
fields
Unit sample space.
Ω :
Type*
Measurable-space structure on `Ω`.
measΩ :
Population measure.
μ :
Measure Ω
`μ` is a probability measure.
probμ :
Realized adoption cohort of each unit (`⊤` = never treated).
Each cohort cell `{G = h}` is measurable.
Gcell_meas :
∀ h, MeasurableSet (G ⁻¹' {h})
Calendar-time map on periods.
time :
Fin T → ℤ
Calendar time is strictly increasing in the period index, so the calendar
order matches the adoption-date order.
time_strictMono :
StrictMono time
Finite adoption cohorts included in the event-study support.
Potential-outcome family: `Ypath t h ω` is the outcome of unit `ω` at
period `t` under adoption path `h`.
**Structural no-anticipation.** In any period where path `h` is untreated
(`absorbingTreatment h t = 0`, i.e. `h = ⊤` or the period precedes adoption),
the outcome under `h` equals the never-treated outcome, for every unit.
def cell reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudyPopulation
The event {ω | G ω = h} for an adoption path.
Definition (Lean source)
def cellMass reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudyPopulation
The population mass of an adoption-path event, as a real number.
Definition (Lean source)
def cellMean reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudyPopulation
Event-level conditional mean on an adoption-path cell. This is totalized by eventCondExp, so zero-mass paths are allowed at the population-bridge layer.
Definition (Lean source)
noncomputable def cellMean (E : EventStudyPopulation T) (f : E.Ω → ℝ)
(h : WithTop (Fin T)) : ℝ :=
eventCondExp E.μ (E.cell h) f
def observed reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudyPopulation
The observed outcome at period t: the potential outcome under the unit's realized adoption path. Consistency is thus definitional.
Definition (Lean source)
def toSystem reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudyPopulation
The event-study system induced by a population: every mean field is the cohort-cell conditional mean of the appropriate potential-outcome slice.
Definition (Lean source)
noncomputable def toSystem (E : EventStudyPopulation T) : EventStudySystem T where
time := E.time
cohorts := E.cohorts
cohortShare h := E.cellMass h
cellMass g _t := E.cellMass (EventStudySystem.finitePath g)
observedPathMean h t := E.cellMean (E.observed t) h
observedMean g t := E.cellMean (E.observed t) (EventStudySystem.finitePath g)
treatedMean g t :=
E.cellMean (E.Ypath t (EventStudySystem.finitePath g))
(EventStudySystem.finitePath g)
untreatedMean g t :=
E.cellMean (E.Ypath t ⊤) (EventStudySystem.finitePath g)
untreatedPathMean h t := E.cellMean (E.Ypath t ⊤) h
def OutcomesIntegrable reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudyPopulation
Outcome integrability (Sun-Abraham assumption H5). Every potential-outcome slice Ypath t h is μ-integrable. This is the population content of the source theorem's integrability hypothesis: it is exactly the condition under which each cohort-cell mean E.cellMean (Ypath t h) · = E[Y_{·t}(h) ∣ G = ·] is a genuine finite expectation rather than only a totalized value. Not every population satisfies it; for example, heavy-tailed potential outcomes can fail this condition.
Definition (Lean source)
def OutcomesIntegrable (E : EventStudyPopulation T) : Prop :=
∀ (t : Fin T) (h : WithTop (Fin T)), Integrable (E.Ypath t h) E.μ
theorem toSystem_CATT_eq_po_contrast reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudyPopulation
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
hypotheses
conclusion
(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)) (EventStudySystem.finitePath g) - E.cellMean (E.Ypath t ⊤) (EventStudySystem.finitePath g))
Proof (Lean source)
theorem toSystem_CATT_eq_po_contrast (E : EventStudyPopulation T)
(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))
(EventStudySystem.finitePath g)
- E.cellMean (E.Ypath t ⊤) (EventStudySystem.finitePath g)) := by
rfl
theorem contamination_representation_population reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudyPopulation
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
hypotheses
E :
D :
(E.toSystem).ConventionalDesign
hPar :
(E.toSystem).MeanParallelUntreated
hSupport :
(E.toSystem).ConventionalFiniteSupport D
hCell :
(E.toSystem).CellGridResidualization D
conclusion
D.mu
= ∑ ge ∈ (E.toSystem).admissibleCells D.eventSupport, (E.toSystem).omega D ge.1 ge.2 * (E.toSystem).CATT ge.1 ge.2
Proof (Lean source)
theorem contamination_representation_population (E : EventStudyPopulation T)
(D : (E.toSystem).ConventionalDesign)
(hPar : (E.toSystem).MeanParallelUntreated)
(hSupport : (E.toSystem).ConventionalFiniteSupport D)
(hCell : (E.toSystem).CellGridResidualization D) :
D.mu =
∑ ge ∈ (E.toSystem).admissibleCells D.eventSupport,
(E.toSystem).omega D ge.1 ge.2 * (E.toSystem).CATT ge.1 ge.2 := by
exact (E.toSystem).contamination_representation_of_cellGrid
E.toSystem_consistency hPar hSupport hCell
theorem IW_convex_characterization_population reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.EventStudyContamination.EventStudyPopulation
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
hypotheses
E :
I :
(E.toSystem).IWDesign
hIWParallelTrends :
(E.toSystem).IWComparisonParallelTrends I
hSupport :
(E.toSystem).IWSupport I
hRhoNonneg :
∀ g ∈ I.cohortsIW, 0 ≤ I.rho g
hRhoSumOne :
∑ g ∈ I.cohortsIW, I.rho g = 1
lo hi :
ℝ
hLo :
∀ g ∈ I.cohortsIW, lo ≤ (E.toSystem).CATT g I.eventTime
hHi :
∀ g ∈ I.cohortsIW, (E.toSystem).CATT g I.eventTime ≤ hi
Proof (Lean source)
theorem IW_convex_characterization_population (E : EventStudyPopulation T)
(I : (E.toSystem).IWDesign)
(hIWParallelTrends : (E.toSystem).IWComparisonParallelTrends I)
(hSupport : (E.toSystem).IWSupport I)
(hRhoNonneg : ∀ g ∈ I.cohortsIW, 0 ≤ I.rho g)
(hRhoSumOne : ∑ g ∈ I.cohortsIW, I.rho g = 1)
{lo hi : ℝ}
(hLo : ∀ g ∈ I.cohortsIW, lo ≤ (E.toSystem).CATT g I.eventTime)
(hHi : ∀ g ∈ I.cohortsIW, (E.toSystem).CATT g I.eventTime ≤ hi) :
(∀ g ∈ I.cohortsIW, (E.toSystem).Delta I g = (E.toSystem).CATT g I.eventTime) ∧
(E.toSystem).nuIW I =
∑ g ∈ I.cohortsIW, I.rho g * (E.toSystem).CATT g I.eventTime ∧
lo ≤ (E.toSystem).nuIW I ∧ (E.toSystem).nuIW I ≤ hi := by
exact (E.toSystem).IW_convex_characterization I
E.toSystem_consistency E.toSystem_noAnticipation E.toSystem_pathConsistency
hIWParallelTrends.hComparisonParallelTrends hSupport hRhoNonneg hRhoSumOne hLo hHi
8 supporting declarations (lemmas, instances)
-
cellMean_congr_ontheorem — Event-level means agree when the integrands agree pointwise on the adoption-path cell.hypothesesconclusionE.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.hypothesesconclusionE.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.hypothesesconclusion∀ ω ∈ E.cell (EventStudySystem.finitePath g),E.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.hypothesesE :hPar :(E.toSystem).MeanParallelUntreatedconclusion(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]