Panel.EstimandCharacterization.HeterogeneousTWFE
de Chaisemartin-D'Haultfœuille: negative-weight diagnostics for TWFE under heterogeneous effects.
FinitePanel 18 core · 11 supporting This file formalizes the finite group-time algebra behind the de Chaisemartin-D'Haultfoeuille two-way fixed-effect estimand. ★ 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
DCDH Finite Panel Algebra
This file formalizes the finite group-time algebra behind the
de Chaisemartin-D'Haultfoeuille two-way fixed-effect estimand. DCDHPanel
packages weighted cells, binary treatment, potential untreated means, treatment
effects, and a residualized-treatment witness. The main results decompose
DCDHPanel.betaTWFE into untreated bias plus treated-cell weighted effects
(twfe_eq_untreatedBias_add_treated_weighted_tau), show that treated DCDH
weights sum to one and have the sign of Dtilde, and prove finite sign-reversal
constructions such as
exists_panel_with_positive_treated_effects_twfe_negative_of_negative_component.
Group-time fixed-effect span, represented as additive group and period components.
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)
Residualized-treatment denominator S_D.
Finite FWL/TWFE coefficient.
Definition (Lean source)
Untreated residual contrast divided by the residualized-treatment denominator.
Definition (Lean source)
Normalized DCDH cell weight, interpreted on treated cells.
Definition (Lean source)
Treated cells {(g,t) | D_gt = 1}.
All-cell treatment-effect component using the binary treatment indicator.
Definition (Lean source)
Treated-cell weighted treatment-effect component.
Definition (Lean source)
Zero untreated residual contrast, the bias-free DCDH condition.
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.hypothesespi 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.Proof (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.hypothesespi 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.Proof (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.Proof (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 < Mconclusion0 < ε ∧ 0 < M ∧ (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 : ι → ℝ, (∀ i, 0 < tau i) ∧ ∑ 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.
Uniform unit-period cell weight 1/(|G|·|T|).
Definition (Lean source)
Builds the uniform balanced-panel DCDH structure whose residualized treatment is the Frisch-Waugh-Lovell double-demeaned 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.Proof (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̈.hypothesesbalanced :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.
Builds a finite DCDH panel from a population model.