Panel.EstimandCharacterization.HeterogeneousTWFE
de Chaisemartin-D'Haultfœuille: negative-weight diagnostics for TWFE under heterogeneous effects.
FinitePanel 18 core · 11 supporting This file develops finite group-by-period algebra for the two-way fixed-effects estimand with heterogeneous treatment effects. ★ twfe_eq_untreatedBias_add_DWeightedTau★ twfe_eq_untreatedBias_add_treated_weighted_tau★ twfe_eq_treated_weighted_tau_of_zeroUntreatedContrast★ treated_omega_sum_eq_one★ treated_omega_neg_iff_Dtilde_neg★ treated_omega_pos_iff_Dtilde_pos★ treated_omega_zero_iff_Dtilde_zero★ exists_panel_with_positive_treated_effects_twfe_negative_of_negative_component
Heterogeneous-effects finite-panel algebra
This file develops finite group-by-period algebra for the two-way fixed-effects estimand with heterogeneous treatment effects. It defines weighted binary-treatment panels, their residualized-treatment coefficient, bias, and effect components, and establishes the decomposition, weight, and sign-reversal results; a companion module supplies their probability-model interpretation.
For group and time index sets and a group-by-time array, the group-time fixed-effect condition holds exactly when the array can be written as the sum of a group-specific component and a time-specific component.
Definition (Lean source)
A finite de Chaisemartin-D'Haultfoeuille group-time panel: it bundles group-time cell weights, a binary treatment indicator, the observed outcome, the untreated potential outcome, cell-level treatment effects, and a residualized-treatment witness, subject to strict positivity and unit sum of the weights, the treatment indicator taking only the values zero and one, potential-outcome consistency — the observed outcome equals the untreated outcome plus the treatment indicator times the treatment effect, the residualized witness differing from the treatment indicator by a group-plus-time additive function, its orthogonality, in the weighted inner product, to every group-plus-time additive function, and a strictly positive weighted sum of its squares.
Definition (Lean source)
For finite group and time sets and a finite DCDH group-time panel, the residualized-treatment denominator is the weighted finite sum of squared residualized treatment values over all group-time cells.
Definition (Lean source)
For finite group and time sets and a finite DCDH group-time panel, the finite TWFE coefficient is the weighted finite inner product of residualized treatment and observed outcome, divided by the residualized-treatment denominator.
Definition (Lean source)
For finite group and time sets and a finite DCDH group-time panel, the untreated residual contrast is the weighted finite inner product of residualized treatment and the untreated potential outcome, divided by the residualized-treatment denominator.
Definition (Lean source)
For finite group and time sets, a finite DCDH group-time panel, a group, and a time period, the normalized DCDH cell weight is that cell's weight times its residualized treatment, divided by the residualized-treatment denominator.
Definition (Lean source)
For finite group and time sets and a finite DCDH group-time panel, the set of treated cells consists exactly of the group-time pairs whose binary treatment indicator equals one.
For finite group and time sets and a finite DCDH group-time panel, the all-cell treatment-effect component is the finite sum of each cell's treatment effect weighted by its cell weight, residualized treatment, and binary treatment indicator, normalized by the denominator.
Definition (Lean source)
For finite group and time sets and a finite DCDH group-time panel, the treated-cell weighted treatment-effect component is the finite sum, over treated cells only, of each normalized DCDH cell weight times that cell's treatment effect.
For finite group and time sets and a finite DCDH group-time panel, the zero untreated residual-contrast condition holds exactly when the weighted finite inner product of residualized treatment and the untreated potential outcome is zero.
Definition (Lean source)
DCDH finite TWFE decomposition (all-cell weighting). For a DCDH panel, the finite two-way fixed-effects (TWFE) coefficient decomposes as the sum of the untreated bias and the all-cell D-weighted treatment-effect component.
Formal statement
Proof (Lean source)
DCDH finite TWFE decomposition (treated-cell weighting). For a DCDH panel, the finite TWFE coefficient decomposes as the sum of the untreated bias and the normalized treated-cell weighted sum of treatment effects.
Formal statement
Proof (Lean source)
Zero untreated bias implies TWFE equals the treated-cell weighted effect. If the untreated-outcome residual contrast vanishes — the residualized-treatment-weighted average of the untreated potential outcome Y0 over the whole panel is zero, then the finite two-way fixed-effects (TWFE) coefficient equals the treated-cell weighted sum of treatment effects.
Formal statement
Proof (Lean source)
DCDH weights sum to one. For a DCDH panel, the normalized DCDH weights sum to one over all treated cells.
Formal statement
Proof (Lean source)
Sign equivalence for the DCDH weight (negative direction). For a DCDH panel and any cohort-period cell, the normalized weight ω_gt is negative exactly when the residualized treatment D̃_gt is negative.
Formal statement
Proof (Lean source)
Positive-weight direction of the DCDH sign characterization. For a DCDH panel and any cohort-period cell, the normalized weight ω_gt is positive exactly when the residualized treatment D̃_gt is positive.
Formal statement
Proof (Lean source)
Zero-weight direction of the DCDH sign characterization. For a DCDH panel and any cohort-period cell, the normalized weight ω_gt is zero exactly when the residualized treatment D̃_gt is zero.
Formal statement
Proof (Lean source)
Panel-level DCDH sign reversal. If the untreated-outcome residual contrast vanishes and the treated cells with negative normalized DCDH weight carry a strictly negative total weight, then there exists another finite DCDH panel — sharing the same cell weights, treatment indicator, untreated potential outcomes, and residualized treatment, but with strictly positive treatment effects on every cell and zero untreated residual contrast — whose two-way fixed-effects (TWFE) coefficient is strictly negative.
Formal statement
Proof (Lean source)
11 supporting declarations (lemmas, instances)
-
inner_Dtilde_D_eq_SD_coretheorem — Orthogonality of the residualized treatment against D - Dtilde gives the DCDH denominator identity.hypothesesG :sharedType u_1T :sharedType u_2pi D Dtilde :G → T → ℝhmem :IsGTFE (fun g t => D g t - Dtilde g t)horth :∀ h : G → T → ℝifIsGTFE hthen∑ g, ∑ t, pi g t * Dtilde g t * h g t = 0conclusion∑ g, ∑ t, pi g t * Dtilde g t * D g t = ∑ g, ∑ t, pi g t * (Dtilde g t)^2Proof (Lean source)
theorem inner_Dtilde_D_eq_SD_core (pi D Dtilde : G → T → ℝ) (hmem : IsGTFE (fun g t => D g t - Dtilde g t)) (horth : ∀ h : G → T → ℝ, IsGTFE h → ∑ g, ∑ t, pi g t * Dtilde g t * h g t = 0) : ∑ g, ∑ t, pi g t * Dtilde g t * D g t = ∑ g, ∑ t, pi g t * (Dtilde g t)^2 := by have horth' : ∑ g, ∑ t, pi g t * Dtilde g t * (D g t - Dtilde g t) = 0 := horth (fun g t => D g t - Dtilde g t) hmem have hdiff : (∑ g, ∑ t, pi g t * Dtilde g t * D g t) - (∑ g, ∑ t, pi g t * (Dtilde g t)^2) = 0 := by rw [← horth'] simp_rw [mul_sub, Finset.sum_sub_distrib, pow_two] ring_nf exact sub_eq_zero.mp hdiff -
inner_Dtilde_D_eq_SDtheorem — Orthogonality of the residualized treatment against D - Dtilde gives the DCDH denominator identity.hypothesesconclusion∑ g, ∑ t, P.pi g t * P.Dtilde g t * P.D g t = P.SDProof (Lean source)
theorem inner_Dtilde_D_eq_SD (P : DCDHPanel G T) : ∑ g, ∑ t, P.pi g t * P.Dtilde g t * P.D g t = P.SD := by simpa [SD] using inner_Dtilde_D_eq_SD_core P.pi P.D P.Dtilde P.D_minus_resid_mem P.Dtilde_orthogonal -
weighted_residual_contrast_eq_zero_of_isGTFEtheorem — A weighted residual is orthogonal to every additive array, so its contrast with an additive untreated-outcome array vanishes.hypothesesG :sharedType u_1T :sharedType u_2pi Dtilde Y0 :G → T → ℝhorth :∀ h : G → T → ℝifIsGTFE hthen∑ g, ∑ t, pi g t * Dtilde g t * h g t = 0hY0 :IsGTFE Y0conclusion∑ g, ∑ t, pi g t * Dtilde g t * Y0 g t = 0Proof (Lean source)
theorem weighted_residual_contrast_eq_zero_of_isGTFE (pi Dtilde Y0 : G → T → ℝ) (horth : ∀ h : G → T → ℝ, IsGTFE h → ∑ g, ∑ t, pi g t * Dtilde g t * h g t = 0) (hY0 : IsGTFE Y0) : ∑ g, ∑ t, pi g t * Dtilde g t * Y0 g t = 0 := horth Y0 hY0 -
zeroUntreatedResidualContrast_of_Y0_mem_gtfetheorem — Group-plus-period untreated means imply the zero untreated residual contrast.hypothesesconclusionP.zeroUntreatedResidualContrastProof (Lean source)
theorem zeroUntreatedResidualContrast_of_Y0_mem_gtfe (P : DCDHPanel G T) (hY0 : IsGTFE P.Y0) : P.zeroUntreatedResidualContrast := by simpa [zeroUntreatedResidualContrast] using weighted_residual_contrast_eq_zero_of_isGTFE P.pi P.Dtilde P.Y0 P.Dtilde_orthogonal hY0 -
DWeightedTau_eq_treatedWeightedTautheorem — The all-cell D-weighted component is the same as the treated-cell sum.hypothesesconclusionP.DWeightedTau = P.treatedWeightedTauProof (Lean source)
theorem DWeightedTau_eq_treatedWeightedTau (P : DCDHPanel G T) : P.DWeightedTau = P.treatedWeightedTau := by unfold DWeightedTau treatedWeightedTau treatedCells omega rw [← Fintype.sum_prod_type' (fun g t => P.pi g t * P.Dtilde g t * P.D g t / P.SD * P.tau g t)] simp_rw [Finset.sum_filter] exact Finset.sum_congr rfl (fun gt _hgt => by rcases gt with ⟨g, t⟩ rcases P.D_binary g t with hD | hD · simp [hD] · simp [hD]) -
normalized_weight_neg_iff_residual_negtheorem — Dividing a positive cell mass times a residual by a positive normalizer preserves whether the residual is negative.hypothesespi Dtilde SD :ℝhpi :0 < pihSD :0 < SDconclusionpi * Dtilde / SD < 0 ↔ Dtilde < 0Proof (Lean source)
theorem normalized_weight_neg_iff_residual_neg {pi Dtilde SD : ℝ} (hpi : 0 < pi) (hSD : 0 < SD) : pi * Dtilde / SD < 0 ↔ Dtilde < 0 := by constructor · intro h have hnum : pi * Dtilde < 0 := ((div_neg_iff.mp h).resolve_left (fun hpos => not_lt_of_gt hSD hpos.2)).1 nlinarith [hpi] · intro h exact div_neg_of_neg_of_pos (mul_neg_of_pos_of_neg hpi h) hSD -
normalized_weight_pos_iff_residual_postheorem — Dividing a positive cell mass times a residual by a positive normalizer preserves whether the residual is positive.hypothesespi Dtilde SD :ℝhpi :0 < pihSD :0 < SDconclusion0 < pi * Dtilde / SD ↔ 0 < DtildeProof (Lean source)
theorem normalized_weight_pos_iff_residual_pos {pi Dtilde SD : ℝ} (hpi : 0 < pi) (hSD : 0 < SD) : 0 < pi * Dtilde / SD ↔ 0 < Dtilde := by rw [div_pos_iff_of_pos_right hSD] constructor · intro h rcases lt_trichotomy Dtilde 0 with h' | h' | h' · exact absurd (mul_neg_of_pos_of_neg hpi h') (not_lt.mpr (le_of_lt h)) · simp [h'] at h · exact h' · intro h exact mul_pos hpi h -
normalized_weight_zero_iff_residual_zerotheorem — A positive cell mass and positive normalizer make the normalized weight zero exactly when its residual is zero.hypothesespi Dtilde SD :ℝhpi :0 < pihSD :0 < SDconclusionpi * Dtilde / SD = 0 ↔ Dtilde = 0Proof (Lean source)
theorem normalized_weight_zero_iff_residual_zero {pi Dtilde SD : ℝ} (hpi : 0 < pi) (hSD : 0 < SD) : pi * Dtilde / SD = 0 ↔ Dtilde = 0 := by rw [div_eq_zero_iff] constructor · intro h rcases h with hnum | hSD0 · rcases mul_eq_zero.mp hnum with hpi0 | hDt · exact absurd hpi0 (ne_of_gt hpi) · exact hDt · exact absurd hSD0 (ne_of_gt hSD) · intro h left rw [h, mul_zero] -
two_cell_signed_weights_positive_effects_negative_sumtheorem — Two-cell signed-weight calculation from the DCDH sign-reversal example.hypothesesc ε M :ℝhc :0 < chε :0 < εhM :((1 + c) * ε) / c < Mconclusionconclusion 10 < εconclusion 20 < Mconclusion 3(1 + c) * ε + (-c) * M < 0Proof (Lean source)
theorem two_cell_signed_weights_positive_effects_negative_sum {c ε M : ℝ} (hc : 0 < c) (hε : 0 < ε) (hM : ((1 + c) * ε) / c < M) : 0 < ε ∧ 0 < M ∧ (1 + c) * ε + (-c) * M < 0 := by constructor · exact hε constructor · have hnum_pos : 0 < (1 + c) * ε := by nlinarith have hfrac_pos : 0 < ((1 + c) * ε) / c := by positivity linarith · have hdom : (1 + c) * ε < c * M := by have hmul := mul_lt_mul_of_pos_left hM hc field_simp [hc.ne'] at hmul nlinarith nlinarith -
exists_positive_effects_negative_weighted_sum_of_negative_componenttheorem — Finite signed-average construction: if normalized weights have a strictly negative component, some strictly positive effects have a negative weighted sum.hypothesesconclusion∃ tau : ι → ℝ,conclusion 1i :0 < tau iconclusion 2∑ i, w i * tau i < 0Proof (Lean source)
theorem exists_positive_effects_negative_weighted_sum_of_negative_component {ι : Type*} [Fintype ι] (w : ι → ℝ) (h_neg_component : ∑ i ∈ (Finset.univ.filter fun i => w i < 0), w i < 0) : ∃ tau : ι → ℝ, (∀ i, 0 < tau i) ∧ ∑ i, w i * tau i < 0 := by classical let N : Finset ι := Finset.univ.filter fun i => w i < 0 let B : ℝ := ∑ i ∈ (Finset.univ.filter fun i => ¬ w i < 0), w i have hAneg : (∑ i ∈ N, w i) < 0 := by simpa [N] using h_neg_component have hden_pos : 0 < -(∑ i ∈ N, w i) := by linarith obtain ⟨M, hM⟩ := exists_gt (max 0 (B / (-(∑ i ∈ N, w i)))) have hMpos : 0 < M := lt_of_le_of_lt (le_max_left _ _) hM have hBlt : B < M * (-(∑ i ∈ N, w i)) := by have hratio : B / (-(∑ i ∈ N, w i)) < M := lt_of_le_of_lt (le_max_right _ _) hM have hmul := mul_lt_mul_of_pos_right hratio hden_pos rw [div_mul_cancel₀ B (ne_of_gt hden_pos)] at hmul simpa [mul_comm, mul_left_comm, mul_assoc] using hmul refine ⟨fun i => if w i < 0 then M else 1, ?_, ?_⟩ · intro i by_cases hi : w i < 0 · simp [hi, hMpos] · simp [hi] · have hsum_split : ∑ i, w i * (if w i < 0 then M else 1) = M * (∑ i ∈ N, w i) + B := by simp only [N, B, Finset.sum_filter] simp_rw [mul_ite, mul_one] rw [Finset.mul_sum, ← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro i _hi by_cases hneg : w i < 0 · simp [hneg] ring · simp [hneg] rw [hsum_split] nlinarith -
neg_component_of_exists_Dtilde_negtheorem — If some treated cell has negative residualized treatment, then the total weight over negatively weighted treated cells is strictly negative.hypothesesP :DCDHPanel G Th :∃ (g : G) (t : T), P.D g t = 1 ∧ P.Dtilde g t < 0Proof (Lean source)
theorem neg_component_of_exists_Dtilde_neg {G T : Type*} [Fintype G] [Fintype T] (P : DCDHPanel G T) (h : ∃ (g : G) (t : T), P.D g t = 1 ∧ P.Dtilde g t < 0) : ∑ gt ∈ (P.treatedCells.filter fun gt => P.omega gt.1 gt.2 < 0), P.omega gt.1 gt.2 < 0 := by obtain ⟨g₀, t₀, hD, hDt⟩ := h let S := P.treatedCells.filter (fun gt => P.omega gt.1 gt.2 < 0) have hmem : (g₀, t₀) ∈ S := by simp only [S, mem_filter, DCDHPanel.treatedCells, mem_filter, Finset.mem_univ, true_and] exact ⟨hD, (DCDHPanel.treated_omega_neg_iff_Dtilde_neg P).mpr hDt⟩ have hle : ∀ gt ∈ S, P.omega gt.1 gt.2 ≤ 0 := fun gt hgt => le_of_lt (Finset.mem_filter.mp hgt).2 -- Finset.sum_lt_sum : (∀ i ∈ s, f i ≤ g i) → (∃ i ∈ s, f i < g i) → sum f < sum g have key : ∑ gt ∈ S, P.omega gt.1 gt.2 < ∑ _gt ∈ S, (0 : ℝ) := Finset.sum_lt_sum hle ⟨(g₀, t₀), hmem, (Finset.mem_filter.mp hmem).2⟩ simpa using key
FWLBridge 3 core · 2 supporting FinitePanel.lean takes the residualized treatment D̃ as a *primitive orthogonality witness*: it merely posits the membership D − D̃ ∈ H_GT, the orthogonality ∑ π D̃ h = 0, and positivity S_D > 0. ★ ofTwoWayPanel★ ofTwoWayPanel_betaTWFE
DCDH residualized treatment as a derived FWL residual
FinitePanel.lean takes the residualized treatment D̃ as a primitive
orthogonality witness: it merely posits the membership D − D̃ ∈ H_GT, the
orthogonality ∑ π D̃ h = 0, and positivity S_D > 0. The paper, however,
derives D̃ as the Frisch–Waugh–Lovell residual of the treatment projected on
the two-way fixed-effect span — i.e. the double-demeaned treatment D̈.
This file verifies, for the uniform balanced panel, that the DCDH residualized
treatment can be constructed from the usual two-way fixed-effect residual. It
builds a genuine DCDHPanel whose Dtilde is the double-demeaned treatment
UniformTwoWayPanel.ddot D, with the membership and orthogonality fields
proved from UniformTwoWayPanel (sub_ddot_eq_unitTimeProjection,
unitTimeProjection_additive, ddot_orthogonal_unit_time) rather than assumed.
Only S_D > 0 (nonzero double-demeaned treatment variation — the genuine
identification input that the treatment is not collinear with the FE span) and
the binary-treatment / consistency primitives remain as hypotheses, exactly as
in the source. No measure theory is used: the construction is pure uniform
finite-panel algebra.
For a finite group set and a finite time set, the uniform group-time cell weight is the reciprocal of the product of their cardinalities.
For finite group and time sets, a balanced panel with at least two groups and two time periods, treatment, observed-outcome, untreated-outcome, and treatment-effect arrays, if treatment is binary in every cell, the observed outcome equals the untreated outcome plus treatment times the treatment effect in every cell, and the weighted sum of squared double-demeaned treatment is strictly positive, then the uniform balanced-panel DCDH structure assigns equal cell weights and uses double-demeaned treatment as its residualized treatment.
Definition (Lean source)
The DCDH TWFE coefficient of the FWL-derived panel equals the uniform-panel Frisch–Waugh–Lovell residualized coefficient of Y on the double-demeaned treatment. For a uniform balanced panel and outcome, treatment, untreated-outcome, and effect arrays Y, D, Y0, tau, suppose the treatment is binary, the observed outcome equals the untreated outcome plus the treatment times the effect (consistency), and the double-demeaned treatment has strictly positive uniformly-weighted variation. Then the two-way fixed-effects (TWFE) coefficient of the DCDH panel built from this data by ofTwoWayPanel equals the Frisch–Waugh–Lovell residualized coefficient of Y regressed on the double-demeaned treatment ddot D.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
uniformWeight_postheorem — For finite nonempty group and time types, the uniform unit-period cell weight is strictly positive.hypothesesG :sharedType u_1T :sharedType u_2Nonempty GNonempty Tconclusion0 < uniformWeight G TProof (Lean source)
theorem uniformWeight_pos [Nonempty G] [Nonempty T] : 0 < uniformWeight G T := by have hG : (0 : ℝ) < (Fintype.card G : ℝ) := by exact_mod_cast (Fintype.card_pos : 0 < Fintype.card G) have hT : (0 : ℝ) < (Fintype.card T : ℝ) := by exact_mod_cast (Fintype.card_pos : 0 < Fintype.card T) exact inv_pos.mpr (mul_pos hG hT) -
ofTwoWayPanel_Dtildetheorem — The residualized treatment of ofTwoWayPanel is exactly the double-demeaned treatment D̈.hypothesesG :sharedType u_1T :sharedType u_2balanced :UniformTwoWayPanel.BalancedPanel G TD Y Y0 tau :G → T → ℝhD_binary :∀ g t, D g t = 0 ∨ D g t = 1hconsistency :∀ g t, Y g t = Y0 g t + D g t * tau g thSD :0 < ∑ g, ∑ t, uniformWeight G T * (ddot D g t) ^ 2conclusion(ofTwoWayPanel balanced D Y Y0 tau hD_binary hconsistency hSD).Dtilde = ddot DProof (Lean source)
@[simp] theorem ofTwoWayPanel_Dtilde (balanced : UniformTwoWayPanel.BalancedPanel G T) (D Y Y0 tau : G → T → ℝ) (hD_binary : ∀ g t, D g t = 0 ∨ D g t = 1) (hconsistency : ∀ g t, Y g t = Y0 g t + D g t * tau g t) (hSD : 0 < ∑ g, ∑ t, uniformWeight G T * (ddot D g t) ^ 2) : (ofTwoWayPanel balanced D Y Y0 tau hD_binary hconsistency hSD).Dtilde = ddot D := rfl
PopulationBridge 1 core · 0 supporting This file connects the finite DCDH panel fields to a probability model with cell events and potential outcomes. ★ ofPopulation
DCDH Population Bridge
This file connects the finite DCDH panel fields to a probability model with cell
events and potential outcomes. The constructor DCDHPanel.ofPopulation builds a
finite panel whose cell weights are cell probabilities, whose Y and Y0 fields
are population cell means, and whose tau field is the difference between the
Y1 and Y0 cell means. Its consistency and pi_sum_one fields are derived
from the shared cell-partition mean-consistency and finite-partition mass
identities.
For finite group and time sets, a measurable sample space with a probability measure, group-time cell events, factual, untreated-potential, and treated-potential outcome functions, a cell-level treatment array, and a residualized-treatment array, if the cells are measurable, pairwise disjoint, and cover the sample space, every cell has strictly positive probability, treatment is binary in every cell, pointwise potential-outcome consistency holds in every cell, treatment minus the residualized array is additive in group and time, the residualized array is weighted-orthogonal to every group-plus-time additive array, and its weighted sum of squares is strictly positive, the finite cell partition supplies cell probabilities and cell means to the finite DCDH panel, whose treatment effects are treated-minus-untreated population cell means.