Panel.EstimandCharacterization.ImputationEventStudy
Borusyak-Jaravel-Spiess: the imputation estimator and the efficiency/characterization results for staggered adoption.
Imputation 16 core · 4 supporting This file gives a finite-cell population formulation of the Borusyak-Jaravel-Spiess imputation functional. ★ bjs_imputation_identification
Borusyak-Jaravel-Spiess Imputation
This file gives a finite-cell population formulation of the
Borusyak-Jaravel-Spiess imputation functional. The core structure BJSPanel
stores treated and untreated cell rows, target weights, observed and untreated
cell means, the untreated-outcome nuisance vector, and treated-cell effects.
It defines the target theta, prediction-span witnesses ImputationWeights,
the observed imputation functional psiImp, and the identification theorem
bjs_imputation_identification. It also defines the finite linear-estimator
API and the witness lemma linear_unbiased_of_imputation_representation; the
substrate-based construction of those witnesses lives in PanelBridge.lean.
For a finite regressor index set, a regressor row, and a nuisance coefficient vector, the finite dot product is the sum, over regressors, of their coordinatewise products.
Definition (Lean source)
A finite treated/untreated cell design for the BJS imputation decomposition, storing treated cells' regressor rows and untreated cells' regressor rows, an arbitrary — possibly signed and non-normalized — target weight on treated cells, the observed-law means on treated and untreated cells, the untreated-potential-outcome means on treated and untreated cells, a nuisance vector for the untreated-outcome model, and treated-cell causal effects.
Definition (Lean source)
For finite treated-cell, untreated-cell, and regressor sets and a BJS panel, the target estimand is the finite sum of each treated cell's causal effect multiplied by its supplied target weight; the weights need not be positive or sum to one.
Definition (Lean source)
For finite treated-cell, untreated-cell, and regressor sets and a BJS panel and an arbitrary treated-cell effect vector, the corresponding target value is the finite sum of that vector weighted by the panel's target weights.
Definition (Lean source)
For finite treated-cell, untreated-cell, and regressor sets and a BJS panel, the untreated-outcome model condition requires that every treated cell's untreated potential-outcome mean equals its regressor-row dot product with the nuisance vector, every untreated cell's untreated potential-outcome mean equals its regressor-row dot product with that vector, and every untreated cell's observed mean equals its untreated potential-outcome mean.
Definition (Lean source)
For finite treated-cell, untreated-cell, and regressor sets and a BJS panel, the fixed-treatment-effect condition requires that in every treated cell the observed mean equals the untreated potential-outcome mean plus that cell's stored treatment effect.
Definition (Lean source)
Witness-form prediction span / imputation weights.
Definition (Lean source)
For finite treated-cell, untreated-cell, and regressor sets and a BJS panel, the target-relevant prediction-identification condition holds exactly when at least one imputation-weight system represents every treated regressor row with nonzero target weight as a weighted combination of untreated regressor rows.
Definition (Lean source)
For finite treated-cell, untreated-cell, and regressor sets and a BJS panel and an array of imputation weights from treated to untreated cells, the observed-law imputation functional is the target-weighted sum of each treated observed mean less its imputed untreated observed mean.
Definition (Lean source)
Population BJS imputation identification. Suppose the untreated outcome mean follows a deterministic linear model in the regressors, and each untreated cell's observed mean equals that untreated model mean (untreated outcome model), there exist imputation weights whose row identity expresses every target-relevant treated cell's regressor row as a weighted combination of untreated-cell rows (target-relevant prediction span), and each treated cell's observed mean equals its untreated potential-outcome mean plus its treatment effect (treatment effect fixed). Then there is an imputation-weight witness for which the observed-law imputation functional psiImp equals the target weighted sum of treatment effects theta.
Formal statement
Proof (Lean source)
A linear functional of treated and untreated observed cell outcomes.
Definition (Lean source)
For finite treated-cell, untreated-cell, and regressor sets and a BJS panel, a linear estimator, an arbitrary array of treated cell outcomes, and an arbitrary array of untreated cell outcomes, the linear-estimator value is the sum of treated outcomes weighted by treated coefficients plus untreated outcomes weighted by untreated coefficients.
Definition (Lean source)
For finite treated-cell, untreated-cell, and regressor sets and a BJS panel and a linear estimator, the observed-law linear-estimator value is its value at the panel's treated and untreated observed means.
Definition (Lean source)
For finite treated-cell, untreated-cell, and regressor sets and a BJS panel, a linear estimator, a nuisance coefficient vector, and an arbitrary treated-effect vector, the model-implied linear-estimator value is its value when treated outcomes equal the regressor prediction plus the effect and untreated outcomes equal the regressor prediction.
Definition (Lean source)
For finite treated-cell, untreated-cell, and regressor sets and a BJS panel and a linear estimator, the unbiasedness condition for all treated effects requires that, for every nuisance coefficient vector and every treated-effect vector, the estimator's model-implied value equals the corresponding target value.
Definition (Lean source)
Explicit imputation representation witness for the linear-unbiased representation helper.
Definition (Lean source)
4 supporting declarations (lemmas, instances)
-
vT_eq_alemma — Unrestricted treatment-effect heterogeneity forces the treated-cell weights to equal the target weights (vT = a). Proved by an indicator-tau test. Hoisted here so the efficiency layer can reuse it without re-running the argument.hypothesesTreated :sharedType u_1Untreated :sharedType u_2L :P.LinearEstimatorh :L.unbiasedForAllTauc :TreatedconclusionL.vT c = P.a cProof (Lean source)
lemma vT_eq_a (L : P.LinearEstimator) (h : L.unbiasedForAllTau) (c : Treated) : L.vT c = P.a c := by classical have hh := h (fun _ : Regressor => 0) (fun d : Treated => if d = c then (1 : ℝ) else 0) simpa [LinearEstimator.modelValue, LinearEstimator.value, targetForTau, dot] using hh -
nuisance_coordlemma — Nuisance unbiasedness for every beta gives the BJS left-null-space coordinate constraint aᵀ Q_T + vUᵀ Q_U = 0 (row by row). Hoisted for the efficiency layer.hypothesesTreated :sharedType u_1Untreated :sharedType u_2L :P.LinearEstimatorh :L.unbiasedForAllTaur :Regressorconclusion(∑ c : Treated, P.a c * P.qT c r) + ∑ u : Untreated, L.vU u * P.qU u r = 0Proof (Lean source)
lemma nuisance_coord (L : P.LinearEstimator) (h : L.unbiasedForAllTau) (r : Regressor) : (∑ c : Treated, P.a c * P.qT c r) + ∑ u : Untreated, L.vU u * P.qU u r = 0 := by classical have hh := h (fun r' : Regressor => if r' = r then (1 : ℝ) else 0) (fun _ : Treated => 0) simpa [LinearEstimator.modelValue, LinearEstimator.value, targetForTau, dot, L.vT_eq_a h] using hh -
linear_unbiased_of_imputation_representation_of_vT_eq_atheorem — Witness-based BJS linear-estimator representation from its treated coefficients and an imputation witness, exposed as an estimator identity for arbitrary outcome arrays.hypothesesTreated :sharedType u_1Untreated :sharedType u_2Regressor :sharedType u_3L :P.LinearEstimatorhVT :∀ c : Treated, L.vT c = P.a chImputationWitness :L.HasImputationRepresentationconclusion∃ H : P.ImputationWeights,conclusion 1c :TreatedL.vT c = P.a cconclusion 2u :UntreatedL.vU u = - ∑ c : Treated, P.a c * H.weight c uconclusion 3YT :Treated → ℝYU :Untreated → ℝL.value YT YU = ∑ c : Treated, P.a c * (YT c - ∑ u : Untreated, H.weight c u * YU u)conclusion 4L.observedValue = P.psiImp H.weightProof (Lean source)
theorem linear_unbiased_of_imputation_representation_of_vT_eq_a (L : P.LinearEstimator) (hVT : ∀ c : Treated, L.vT c = P.a c) (hImputationWitness : L.HasImputationRepresentation) : ∃ H : P.ImputationWeights, (∀ c : Treated, L.vT c = P.a c) ∧ (∀ u : Untreated, L.vU u = - ∑ c : Treated, P.a c * H.weight c u) ∧ (∀ (YT : Treated → ℝ) (YU : Untreated → ℝ), L.value YT YU = ∑ c : Treated, P.a c * (YT c - ∑ u : Untreated, H.weight c u * YU u)) ∧ L.observedValue = P.psiImp H.weight := by classical let H : P.ImputationWeights := hImputationWitness.weights have hVU : ∀ u : Untreated, L.vU u = - ∑ c : Treated, P.a c * H.weight c u := by intro u exact hImputationWitness.untreated_weight_representation u have hValue : ∀ (YT : Treated → ℝ) (YU : Untreated → ℝ), L.value YT YU = ∑ c : Treated, P.a c * (YT c - ∑ u : Untreated, H.weight c u * YU u) := by intro YT YU unfold LinearEstimator.value rw [show (∑ c : Treated, L.vT c * YT c) = ∑ c : Treated, P.a c * YT c from by apply Finset.sum_congr rfl intro c hc rw [hVT c]] rw [show (∑ u : Untreated, L.vU u * YU u) = ∑ u : Untreated, (-(∑ c : Treated, P.a c * H.weight c u)) * YU u from by apply Finset.sum_congr rfl intro u hu rw [hVU u]] have hNeg : (∑ u : Untreated, (-(∑ c : Treated, P.a c * H.weight c u)) * YU u) = -∑ u : Untreated, (∑ c : Treated, P.a c * H.weight c u) * YU u := by calc (∑ u : Untreated, (-(∑ c : Treated, P.a c * H.weight c u)) * YU u) = ∑ u : Untreated, -((∑ c : Treated, P.a c * H.weight c u) * YU u) := by apply Finset.sum_congr rfl intro u hu rw [neg_mul] _ = -∑ u : Untreated, (∑ c : Treated, P.a c * H.weight c u) * YU u := by rw [Finset.sum_neg_distrib] have hReindex : (∑ u : Untreated, (∑ c : Treated, P.a c * H.weight c u) * YU u) = ∑ c : Treated, ∑ u : Untreated, (P.a c * H.weight c u) * YU u := by calc (∑ u : Untreated, (∑ c : Treated, P.a c * H.weight c u) * YU u) = ∑ u : Untreated, ∑ c : Treated, (P.a c * H.weight c u) * YU u := by apply Finset.sum_congr rfl intro u hu rw [Finset.sum_mul] _ = ∑ c : Treated, ∑ u : Untreated, (P.a c * H.weight c u) * YU u := by rw [Finset.sum_comm] calc (∑ c : Treated, P.a c * YT c) + ∑ u : Untreated, (-(∑ c : Treated, P.a c * H.weight c u)) * YU u = (∑ c : Treated, P.a c * YT c) - ∑ u : Untreated, (∑ c : Treated, P.a c * H.weight c u) * YU u := by rw [hNeg, sub_eq_add_neg] _ = (∑ c : Treated, P.a c * YT c) - ∑ c : Treated, ∑ u : Untreated, (P.a c * H.weight c u) * YU u := by rw [hReindex] _ = ∑ c : Treated, (P.a c * YT c - ∑ u : Untreated, (P.a c * H.weight c u) * YU u) := by rw [Finset.sum_sub_distrib] _ = ∑ c : Treated, P.a c * (YT c - ∑ u : Untreated, H.weight c u * YU u) := by apply Finset.sum_congr rfl intro c hc rw [mul_sub] congr rw [Finset.mul_sum] apply Finset.sum_congr rfl intro u hu rw [mul_assoc] refine ⟨H, hVT, hVU, hValue, ?_⟩ unfold LinearEstimator.observedValue psiImp exact hValue P.EY_T P.EY_U -
linear_unbiased_of_imputation_representationtheorem — Universal unbiasedness supplies the treated-coefficient identity required by linear_unbiased_of_imputation_representation_of_vT_eq_a.hypothesesTreated :sharedType u_1Untreated :sharedType u_2Regressor :sharedType u_3L :P.LinearEstimatorhUnbiasedForAllTau :L.unbiasedForAllTauhImputationWitness :L.HasImputationRepresentationconclusion∃ H : P.ImputationWeights,conclusion 1c :TreatedL.vT c = P.a cconclusion 2u :UntreatedL.vU u = - ∑ c : Treated, P.a c * H.weight c uconclusion 3YT :Treated → ℝYU :Untreated → ℝL.value YT YU = ∑ c : Treated, P.a c * (YT c - ∑ u : Untreated, H.weight c u * YU u)conclusion 4L.observedValue = P.psiImp H.weightProof (Lean source)
theorem linear_unbiased_of_imputation_representation (L : P.LinearEstimator) (hUnbiasedForAllTau : L.unbiasedForAllTau) (hImputationWitness : L.HasImputationRepresentation) : ∃ H : P.ImputationWeights, (∀ c : Treated, L.vT c = P.a c) ∧ (∀ u : Untreated, L.vU u = - ∑ c : Treated, P.a c * H.weight c u) ∧ (∀ (YT : Treated → ℝ) (YU : Untreated → ℝ), L.value YT YU = ∑ c : Treated, P.a c * (YT c - ∑ u : Untreated, H.weight c u * YU u)) ∧ L.observedValue = P.psiImp H.weight := by classical apply linear_unbiased_of_imputation_representation_of_vT_eq_a P L ?_ hImputationWitness intro c have h := hUnbiasedForAllTau (fun _ : Regressor => 0) (fun d : Treated => if d = c then (1 : ℝ) else 0) simpa [LinearEstimator.modelValue, LinearEstimator.value, targetForTau, dot] using h
Efficiency 5 core · 3 supporting This file connects the finite BJS imputation design to Gauss-Markov efficiency. ★ bjs_ols_imputation_min_variance_spherical
Borusyak-Jaravel-Spiess Efficiency
This file connects the finite BJS imputation design to Gauss-Markov efficiency. It builds the full event-study design matrix and proves that the OLS imputation weights attain no larger variance than any linear unbiased estimator under spherical cell-outcome errors.
For a BJS event-study panel with finite treated cells, untreated cells, and regressors, the full event-study design matrix has one row for each treated or untreated observed cell and one column for each treated-cell effect or regressor. A treated-cell row has its own effect indicator and its treated-cell regressor row, whereas an untreated-cell row has zero effect indicators and its untreated-cell regressor row.
Definition (Lean source)
For a BJS event-study panel with finite treated cells, untreated cells, and regressors, the target functional in full-design coordinates assigns the panel's target weight to each treated-cell-effect coordinate and zero to every regressor coordinate.
For a linear estimator of a BJS event-study panel with finite cell sets, the weight vector over all observed cells equals its treated-cell weights on treated cells and its untreated-cell weights on untreated cells.
BJS efficiency: OLS imputation is BLUE under spherical errors. For a BJS event-study panel P and a family of cell outcomes Y on a probability space, suppose each cell outcome is square-integrable, the cell outcomes form a spherical family with common variance σ² — equal variances and zero cross-covariances, and the full event-study design matrix designFull P has full column rank. Then for any linear estimator L unbiased for every value of the treatment-effect vector, the variance of the OLS imputation estimator built from designFull P and the target functional cFull P is no larger than the variance of L.
Formal statement
Proof (Lean source)
The treated-cell classifier maps each treated observed cell to its own treated-cell label and maps every untreated observed cell to no label.
3 supporting declarations (lemmas, instances)
-
weightOf_vecMul_designFulllemma — Unbiasedness bridge. A linear estimator is unbiased for every tau iff its weight vector satisfies the design constraint w ᵥ* designFull = cFull. (Only the forward direction is needed below, but it captures both vT = a and the nuisance left-null constraint.)hypothesesTreated :sharedType u_1Untreated :sharedType u_2L :P.LinearEstimatorh :L.unbiasedForAllTauconclusionProof (Lean source)
lemma weightOf_vecMul_designFull {P : BJSPanel Treated Untreated Regressor} (L : P.LinearEstimator) (h : L.unbiasedForAllTau) : weightOf L ᵥ* designFull P = cFull P := by classical funext j have hsplit : (weightOf L ᵥ* designFull P) j = (∑ c : Treated, weightOf L (inl c) * designFull P (inl c) j) + ∑ u : Untreated, weightOf L (inr u) * designFull P (inr u) j := by simp only [vecMul, dotProduct, Fintype.sum_sum_type] rw [hsplit] cases j with | inl d => simp only [weightOf, designFull, Matrix.of_apply, Sum.elim_inl, Sum.elim_inr, cFull, mul_ite, mul_one, mul_zero, Finset.sum_ite_eq', Finset.mem_univ, if_true, Finset.sum_const_zero, add_zero] exact L.vT_eq_a h d | inr r => simp only [weightOf, designFull, Matrix.of_apply, Sum.elim_inl, Sum.elim_inr, cFull] rw [show (∑ c : Treated, L.vT c * P.qT c r) = ∑ c : Treated, P.a c * P.qT c r from Finset.sum_congr rfl (fun c _ => by rw [L.vT_eq_a h c])] exact L.nuisance_coord h r -
designFull_col_eq_cellIndicatorlemma — Each treated-cell fixed-effect column of designFull is the panel cell indicator of treatedClassifier.hypothesesTreated :sharedType u_1Untreated :sharedType u_2Regressor :sharedType u_3P :BJSPanel Treated Untreated Regressord :Treatedconclusion(fun i => designFull P i (inl d))= cellIndicator (treatedClassifier (Untreated := Untreated)) (some d)Proof (Lean source)
lemma designFull_col_eq_cellIndicator (P : BJSPanel Treated Untreated Regressor) (d : Treated) : (fun i => designFull P i (inl d)) = cellIndicator (treatedClassifier (Untreated := Untreated)) (some d) := by funext i cases i with | inl c => simp [designFull, treatedClassifier, cellIndicator] | inr u => simp [designFull, treatedClassifier, cellIndicator] -
designFull_col_mem_indicatorSpanlemma — The treated-cell fixed-effect block of designFull lies in the panel IndicatorSpan of the treated-cell classifier: the BJS event-study FE design is the panel indicator-span substrate.hypothesesTreated :sharedType u_1Untreated :sharedType u_2Regressor :sharedType u_3P :BJSPanel Treated Untreated Regressord :TreatedconclusionProof (Lean source)
lemma designFull_col_mem_indicatorSpan (P : BJSPanel Treated Untreated Regressor) (d : Treated) : (fun i => designFull P i (inl d)) ∈ indicatorSpan (treatedClassifier (Untreated := Untreated)) := by rw [designFull_col_eq_cellIndicator] exact cellIndicator_mem_indicatorSpan _ _
PanelBridge 4 core · 5 supporting This file connects the finite imputation event-study construction to the library's weighted-panel linear algebra. ★ bjs_linear_unbiased_iff_imputation_form
Imputation event-study linear-algebra bridge
This file connects the finite imputation event-study construction to the library's weighted-panel linear algebra. It equips untreated cells with uniform weights, forms the span of their regressor columns, identifies the usual left-null-space restriction with orthogonality to that span, and derives the corresponding linear-unbiasedness characterizations.
For a nonempty finite collection of untreated cells, the uniform untreated-cell weighted support assigns every untreated cell weight and regards every such cell as observed.
Definition (Lean source)
For a BJS event-study panel with finite treated cells, untreated cells, and regressors and a regressor, the corresponding untreated-cell regressor column assigns to each untreated cell its entry in that regressor's panel row.
Definition (Lean source)
For a BJS event-study panel with finite treated cells, untreated cells, and regressors, the untreated-cell regressor column span is the real linear span of all vectors of untreated-cell regressor values, one vector for each regressor.
Combined iff characterization of the BJS linear-unbiased imputation class. Given a target-relevant prediction-span witness and at least one treated cell with nonzero target weight, a linear estimator L is unbiased for every value of the treatment-effect vector if and only if it admits a BJS imputation-weight representation: its treated coefficients match the target weights, its untreated coefficients equal the negative weighted imputation sum, its value equals the imputation contrast for every pair of treated/untreated observed outcomes, and its observed value equals the population imputation functional psiImp.
Formal statement
Proof (Lean source)
5 supporting declarations (lemmas, instances)
-
ip_untreatedSupport_regressorColumnlemma — The panel inner product of an untreated-cell vector v with a regressor column is the BJS left-null-space sum, rescaled by the uniform weight.hypothesesTreated :sharedType u_1Untreated :sharedType u_2Regressor :sharedType u_3v :Untreated → ℝr :Regressorconclusion(untreatedSupport Untreated).ip v (P.regressorColumn r)= (Fintype.card Untreated : ℝ)⁻¹ * ∑ u : Untreated, v u * P.qU u rProof (Lean source)
lemma ip_untreatedSupport_regressorColumn (v : Untreated → ℝ) (r : Regressor) : (untreatedSupport Untreated).ip v (P.regressorColumn r) = (Fintype.card Untreated : ℝ)⁻¹ * ∑ u : Untreated, v u * P.qU u r := by rw [WeightedSupport.ip_def, Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro u _ simp only [untreatedSupport, regressorColumn] ring -
ip_regressorColumn_eq_zero_ifflemma — ip-orthogonality to a single regressor column ⟺ that column's BJS left-null-space coordinate vanishes.hypothesesTreated :sharedType u_1Untreated :sharedType u_2Regressor :sharedType u_3v :Untreated → ℝr :Regressorconclusion(untreatedSupport Untreated).ip v (P.regressorColumn r)= 0 ↔ ∑ u : Untreated, v u * P.qU u r = 0Proof (Lean source)
lemma ip_regressorColumn_eq_zero_iff (v : Untreated → ℝ) (r : Regressor) : (untreatedSupport Untreated).ip v (P.regressorColumn r) = 0 ↔ ∑ u : Untreated, v u * P.qU u r = 0 := by rw [ip_untreatedSupport_regressorColumn] rw [mul_eq_zero] have hne : (Fintype.card Untreated : ℝ)⁻¹ ≠ 0 := by simp [Fintype.card_ne_zero] constructor · rintro (h | h) · exact absurd h hne · exact h · intro h; exact inr h -
columnSpan_ip_orthogonal_ifflemma — Keystone bridge. A vector over the untreated cells is ip-orthogonal to the whole regressor column span iff it satisfies the BJS left-null-space condition ∀ r, ∑_u v_u q_{ur} = 0. This is the panel-substrate restatement of "v lies in the left null space of Q_U".hypothesesTreated :sharedType u_1Untreated :sharedType u_2Regressor :sharedType u_3v :Untreated → ℝconclusion(∀ h ∈ P.columnSpan, (untreatedSupport Untreated).ip v h = 0)↔ ∀ r : Regressor, ∑ u : Untreated, v u * P.qU u r = 0Proof (Lean source)
lemma columnSpan_ip_orthogonal_iff (v : Untreated → ℝ) : (∀ h ∈ P.columnSpan, (untreatedSupport Untreated).ip v h = 0) ↔ ∀ r : Regressor, ∑ u : Untreated, v u * P.qU u r = 0 := by constructor · intro h r rw [← ip_regressorColumn_eq_zero_iff] exact h (P.regressorColumn r) (Submodule.subset_span ⟨r, rfl⟩) · intro h have hcol : ∀ r : Regressor, (untreatedSupport Untreated).ip v (P.regressorColumn r) = 0 := by intro r; rw [ip_regressorColumn_eq_zero_iff]; exact h r -- The set of `w` with `ip v w = 0` is a submodule containing every column, -- hence contains the whole span. intro w hw refine Submodule.span_induction ?_ ?_ ?_ ?_ hw · rintro x ⟨r, rfl⟩; exact hcol r · simp [WeightedSupport.ip] · intro x y _ _ hx hy rw [WeightedSupport.ip_add_right, hx, hy, add_zero] · intro s x _ hx rw [WeightedSupport.ip_smul_right, hx, mul_zero] -
exists_imputationWeights_of_gap_orthogonaltheorem — Left-null-space row adjustment (audit M3), phrased through the panel substrate. Given base imputation weights H0, a nonzero target weight at c0, and a target untreated-coefficient vector vU whose gap gap u = vU u + ∑_c a_c · H0.weight c u is ip-orthogonal to the regressor column span (equivalently: gap lies in the left null space of Q_U), one nonzero target row of H0 can absorb the gap without disturbing any target-relevant row identity. The resulting imputation weights H represent the untreated coefficients: ∑_c a_c · H.weight c u = - vU u for every u.hypothesesTreated :sharedType u_1Untreated :sharedType u_2Regressor :sharedType u_3vU :Untreated → ℝc0 :Treatedhc0 :P.a c0 ≠ 0H0 :P.ImputationWeightshgap :∀ h ∈ P.columnSpan,(untreatedSupport Untreated).ip (fun u => vU u + ∑ c : Treated, P.a c * H0.weight c u) h= 0conclusion∃ H : P.ImputationWeights, ∀ u : Untreated, (∑ c : Treated, P.a c * H.weight c u) = - vU uProof (Lean source)
theorem exists_imputationWeights_of_gap_orthogonal (vU : Untreated → ℝ) {c0 : Treated} (hc0 : P.a c0 ≠ 0) (H0 : P.ImputationWeights) (hgap : ∀ h ∈ P.columnSpan, (untreatedSupport Untreated).ip (fun u => vU u + ∑ c : Treated, P.a c * H0.weight c u) h = 0) : ∃ H : P.ImputationWeights, ∀ u : Untreated, (∑ c : Treated, P.a c * H.weight c u) = - vU u := by classical let weightedUntreated : Untreated → ℝ := fun u => ∑ c : Treated, P.a c * H0.weight c u let correction : Untreated → ℝ := fun u => (P.a c0)⁻¹ * (-vU u - weightedUntreated u) -- The panel-substrate orthogonality hypothesis unpacks (via the keystone -- bridge) to the BJS left-null-space coordinate condition on the gap. have hWeightedCombined : ∀ r : Regressor, ∑ u : Untreated, (vU u + weightedUntreated u) * P.qU u r = 0 := (P.columnSpan_ip_orthogonal_iff _).mp hgap have hCorrectionNull : ∀ r : Regressor, ∑ u : Untreated, correction u * P.qU u r = 0 := by intro r have hNeg : ∑ u : Untreated, (-vU u - weightedUntreated u) * P.qU u r = 0 := by calc (∑ u : Untreated, (-vU u - weightedUntreated u) * P.qU u r) = -∑ u : Untreated, (vU u + weightedUntreated u) * P.qU u r := by rw [← Finset.sum_neg_distrib] apply Finset.sum_congr rfl intro u _ ring _ = 0 := by rw [hWeightedCombined r, neg_zero] calc (∑ u : Untreated, correction u * P.qU u r) = (P.a c0)⁻¹ * ∑ u : Untreated, (-vU u - weightedUntreated u) * P.qU u r := by simp only [correction] rw [Finset.mul_sum] apply Finset.sum_congr rfl intro u _ rw [mul_assoc] _ = 0 := by rw [hNeg, mul_zero] let HWeight : Treated → Untreated → ℝ := fun c u => if c = c0 then H0.weight c u + correction u else H0.weight c u have hHWeightSum : ∀ u : Untreated, (∑ c : Treated, P.a c * HWeight c u) = -vU u := by intro u have hUpdate : (∑ c : Treated, P.a c * HWeight c u) = (∑ c : Treated, P.a c * H0.weight c u) + P.a c0 * correction u := by calc (∑ c : Treated, P.a c * HWeight c u) = ∑ c : Treated, (P.a c * H0.weight c u + if c = c0 then P.a c * correction u else 0) := by apply Finset.sum_congr rfl intro c _ by_cases hC : c = c0 · subst c; simp [HWeight]; ring · simp [HWeight, hC] _ = (∑ c : Treated, P.a c * H0.weight c u) + ∑ c : Treated, (if c = c0 then P.a c * correction u else 0) := by rw [Finset.sum_add_distrib] _ = (∑ c : Treated, P.a c * H0.weight c u) + P.a c0 * correction u := by simp calc (∑ c : Treated, P.a c * HWeight c u) = weightedUntreated u + P.a c0 * correction u := by rw [hUpdate] _ = weightedUntreated u + P.a c0 * ((P.a c0)⁻¹ * (-vU u - weightedUntreated u)) := rfl _ = -vU u := by rw [← mul_assoc, mul_inv_cancel₀ hc0, one_mul]; ring refine ⟨{ weight := HWeight, row_identity := ?_ }, hHWeightSum⟩ intro c hA r by_cases hC : c = c0 · subst c calc (∑ u : Untreated, HWeight c0 u * P.qU u r) = ∑ u : Untreated, (H0.weight c0 u + correction u) * P.qU u r := by simp [HWeight] _ = (∑ u : Untreated, H0.weight c0 u * P.qU u r) + ∑ u : Untreated, correction u * P.qU u r := by rw [← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro u _; rw [add_mul] _ = P.qT c0 r := by rw [H0.row_identity c0 hc0 r, hCorrectionNull r, add_zero] · simpa [HWeight, hC] using H0.row_identity c hA r -
linear_unbiased_of_prediction_identifiedtheorem — BJS linear-unbiased representation from the primitive prediction-span condition.hypothesesTreated :sharedType u_1Untreated :sharedType u_2Regressor :sharedType u_3L :P.LinearEstimatorhUnbiasedForAllTau :L.unbiasedForAllTauhPredictionSpan :P.PredictionIdentifiedhNonzeroTargetWeight :∃ c : Treated, P.a c ≠ 0conclusion∃ H : P.ImputationWeights,conclusion 1c :TreatedL.vT c = P.a cconclusion 2u :UntreatedL.vU u = - ∑ c : Treated, P.a c * H.weight c uconclusion 3YT :Treated → ℝYU :Untreated → ℝL.value YT YU = ∑ c : Treated, P.a c * (YT c - ∑ u : Untreated, H.weight c u * YU u)conclusion 4L.observedValue = P.psiImp H.weightProof (Lean source)
theorem linear_unbiased_of_prediction_identified (L : P.LinearEstimator) (hUnbiasedForAllTau : L.unbiasedForAllTau) (hPredictionSpan : P.PredictionIdentified) (hNonzeroTargetWeight : ∃ c : Treated, P.a c ≠ 0) : ∃ H : P.ImputationWeights, (∀ c : Treated, L.vT c = P.a c) ∧ (∀ u : Untreated, L.vU u = - ∑ c : Treated, P.a c * H.weight c u) ∧ (∀ (YT : Treated → ℝ) (YU : Untreated → ℝ), L.value YT YU = ∑ c : Treated, P.a c * (YT c - ∑ u : Untreated, H.weight c u * YU u)) ∧ L.observedValue = P.psiImp H.weight := by classical haveI : DecidableEq Untreated := Classical.decEq Untreated let H0 : P.ImputationWeights := choice hPredictionSpan rcases hNonzeroTargetWeight with ⟨c0, hc0⟩ have hVT : ∀ c : Treated, L.vT c = P.a c := by intro c have h := hUnbiasedForAllTau (fun _ : Regressor => 0) (fun d : Treated => if d = c then (1 : ℝ) else 0) simpa [LinearEstimator.modelValue, LinearEstimator.value, targetForTau, dot] using h let weightedUntreated : Untreated → ℝ := fun u => ∑ c : Treated, P.a c * H0.weight c u have hNuisanceCoord : ∀ r : Regressor, (∑ c : Treated, P.a c * P.qT c r) + ∑ u : Untreated, L.vU u * P.qU u r = 0 := by intro r let beta : Regressor → ℝ := fun r' => if r' = r then (1 : ℝ) else 0 have h := hUnbiasedForAllTau beta (fun _ : Treated => 0) simpa [LinearEstimator.modelValue, LinearEstimator.value, targetForTau, dot, beta, hVT] using h have hH0Aggregate : ∀ r : Regressor, (∑ c : Treated, P.a c * P.qT c r) = ∑ u : Untreated, weightedUntreated u * P.qU u r := by intro r calc (∑ c : Treated, P.a c * P.qT c r) = ∑ c : Treated, P.a c * ∑ u : Untreated, H0.weight c u * P.qU u r := by apply Finset.sum_congr rfl intro c hc by_cases hA : P.a c = 0 · simp [hA] · rw [H0.row_identity c hA r] _ = ∑ c : Treated, ∑ u : Untreated, P.a c * (H0.weight c u * P.qU u r) := by apply Finset.sum_congr rfl intro c hc rw [Finset.mul_sum] _ = ∑ u : Untreated, ∑ c : Treated, P.a c * (H0.weight c u * P.qU u r) := by rw [Finset.sum_comm] _ = ∑ u : Untreated, weightedUntreated u * P.qU u r := by apply Finset.sum_congr rfl intro u hu unfold weightedUntreated rw [Finset.sum_mul] apply Finset.sum_congr rfl intro c hc rw [mul_assoc] have hWeightedCombined : ∀ r : Regressor, ∑ u : Untreated, (L.vU u + weightedUntreated u) * P.qU u r = 0 := by intro r have hN := hNuisanceCoord r rw [hH0Aggregate r] at hN calc (∑ u : Untreated, (L.vU u + weightedUntreated u) * P.qU u r) = (∑ u : Untreated, L.vU u * P.qU u r) + ∑ u : Untreated, weightedUntreated u * P.qU u r := by rw [← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro u hu rw [add_mul] _ = (∑ u : Untreated, weightedUntreated u * P.qU u r) + ∑ u : Untreated, L.vU u * P.qU u r := by rw [add_comm] _ = 0 := hN -- With no untreated cells the imputation representation is vacuous on the -- untreated coordinates; otherwise route the gap through the panel substrate. rcases isEmpty_or_nonempty Untreated with hEmpty | hNE · have hWitness : L.HasImputationRepresentation := { weights := H0 untreated_weight_representation := by intro u; exact (hEmpty.false u).elim } exact linear_unbiased_of_imputation_representation P L hUnbiasedForAllTau hWitness · have hgap : ∀ h ∈ P.columnSpan, (untreatedSupport Untreated).ip (fun u => L.vU u + ∑ c : Treated, P.a c * H0.weight c u) h = 0 := by rw [P.columnSpan_ip_orthogonal_iff] intro r exact hWeightedCombined r obtain ⟨H, hHsum⟩ := P.exists_imputationWeights_of_gap_orthogonal L.vU hc0 H0 hgap have hWitness : L.HasImputationRepresentation := { weights := H untreated_weight_representation := by intro u; rw [hHsum u]; ring } exact linear_unbiased_of_imputation_representation P L hUnbiasedForAllTau hWitness
PanelGrounding 5 core · 8 supporting Builds a BJSPanel from an adoption path and two-way fixed effects, and proves the untreated-outcome model and fixed-effect hypotheses hold for it. ★ ofStaggeredTWFE_untreatedModel
BJS staggered-adoption grounding
Builds a BJSPanel from an adoption path and two-way fixed effects, and proves
the untreated-outcome model and fixed-effect hypotheses hold for it. Treated
cells are the cells whose treatment has switched on, untreated cells include
never-treated cells and pre-adoption cells, and the canonical two-way
fixed-effect design discharges the BJS hypotheses in a concrete panel. The main
definitions are TreatedCell, UntreatedCell, feRow, and
ofStaggeredTWFE; the main theorem bridges are
ofStaggeredTWFE_untreatedModel and ofStaggeredTWFE_treatmentFixed.
For an adoption-time path for the units over a finite number of periods, the treated cells are precisely the unit-period pairs for which the unit's adoption time is no later than the period.
For an adoption-time path for the units over a finite number of periods, the untreated cells are precisely the unit-period pairs whose period is strictly before the unit's adoption time. They include every period of a never-treated unit and every pre-adoption period of a treated unit.
For a unit-period cell with a finite number of periods and equality-comparable unit labels, the two-way fixed-effect design row assigns one to that cell's unit coordinate and period coordinate, and zero to all other unit and period coordinates.
For an adoption-time path for finitely many equality-comparable units over a finite number of periods, unit effects, period effects, target weights, and treated-cell effects, the staggered-adoption two-way-fixed-effects BJS panel has treated and untreated cells given by that path and regressors given by the unit and period indicators. Its untreated potential-outcome mean is the sum of the relevant unit and period effects, and its treated observed mean adds the treated-cell effect.
Definition (Lean source)
Untreated-outcome model holds by construction. For unit fixed effects α, period fixed effects lam, and target weights and treated-cell effects a, tau, the staggered-adoption grounded panel ofStaggeredTWFE g α lam a tau satisfies the BJS untreated-outcome model: treated and untreated cell means both equal the two-way fixed-effect model α_i + λ_t, and untreated cells exhibit no anticipation.
Formal statement
Proof (Lean source)
8 supporting declarations (lemmas, instances)
-
instDecidablePredProdFinLeFstSndinstance — For an adoption-time path for the units over a finite number of periods, a decision procedure for the treated-cell condition determines, for every unit-period cell, whether the unit's adoption time is no later than that period.parametersinstanceinstDecidablePredProdFinLeFstSnd g :DecidablePred (fun c : I × Fin T => AdoptionPath.le (g c.1) c.2)given byby intro c; unfold AdoptionPath.le; infer_instance -
instDecidablePredProdFinLtFstSndinstance — For an adoption-time path for the units over a finite number of periods, a decision procedure for the untreated-cell condition determines, for every unit-period cell, whether the period is strictly before the unit's adoption time.parametersinstanceinstDecidablePredProdFinLtFstSnd g :DecidablePred (fun c : I × Fin T => AdoptionPath.lt (g c.1) c.2)given byby intro c; unfold AdoptionPath.lt; infer_instance -
instFintypeTreatedCellinstance — For an adoption-time path for a finite population over a finite number of periods, a finite enumeration of the treated cells is available. -
instFintypeUntreatedCellinstance — For an adoption-time path for a finite population over a finite number of periods, a finite enumeration of the untreated cells is available. -
treated_not_untreatedtheorem — The cell partition is exclusive: no cell is both adopted-by-t and untreated-at-t.hypothesesI :sharedType u_1T :sharedℕc :I × Fin ThT :AdoptionPath.le (g c.1) c.2hU :AdoptionPath.lt (g c.1) c.2conclusionProof (Lean source)
theorem treated_not_untreated {c : I × Fin T} (hT : AdoptionPath.le (g c.1) c.2) (hU : AdoptionPath.lt (g c.1) c.2) : False := AdoptionPath.not_le_of_lt hU hT -
treated_or_untreatedtheorem — The cell partition is exhaustive: every cell is treated or untreated.hypothesesconclusionAdoptionPath.le (g c.1) c.2 ∨ AdoptionPath.lt (g c.1) c.2Proof (Lean source)
-
dot_feRowlemma — The two-way FE row evaluates the additive fixed-effect model: q_{(i,t)} · (α, λ) = α_i + λ_t.hypotheses -
ofStaggeredTWFE_treatmentFixedtheorem — The grounded panel satisfies the BJS fixed-effect equation E[Y_T] = E[Y_T(0)] + τ.hypothesesconclusion(ofStaggeredTWFE g α lam a tau).TreatmentEffectFixedProof (Lean source)
theorem ofStaggeredTWFE_treatmentFixed (α : I → ℝ) (lam : Fin T → ℝ) (a tau : TreatedCell g → ℝ) : (ofStaggeredTWFE g α lam a tau).TreatmentEffectFixed := fun _ => rfl
PopulationBridge 4 core · 5 supporting This file constructs a finite BJSPanel from a probability space with treated and untreated potential outcomes, defining its mean fields as treated/untreated cell conditional means and deriving the untreated-consistency a ★ bjs_imputation_identification_population
Borusyak-Jaravel-Spiess imputation population bridge
This file constructs a finite BJSPanel from a probability space with treated
and untreated potential outcomes, defining its mean fields as treated/untreated
cell conditional means and deriving the untreated-consistency and fixed-effect
restrictions from cell-level potential-outcome consistency.
A population for the BJS imputation design: a probability space with a treated/untreated cell classifier and potential outcomes Y0 (untreated), Y1 (treated), and observed Yobs, related by cell-level consistency. The design rows qT, qU, target weights a, and nuisance vector beta0 are carried through to the induced panel unchanged.
Definition (Lean source)
For a BJS population with finite treated-cell, untreated-cell, and regressor collections, the treated-and-untreated cell partition partitions its sample space according to the population's treated/untreated cell classifier, using the population probability measure.
Definition (Lean source)
For a BJS population with finite treated-cell, untreated-cell, and regressor collections, the induced BJS panel retains its regressor rows, target weights, and nuisance vector, and defines each outcome mean as the corresponding treated- or untreated-cell conditional mean. For every treated cell, its treatment effect is the conditional mean of the treated potential outcome minus that of the untreated potential outcome.
Definition (Lean source)
Population BJS imputation identification (headline). For a population BJS design E, suppose the conditional mean of the untreated potential outcome on each treated cell equals a linear function q_T · β₀ of the treated-cell regressors and likewise, on each untreated cell, the conditional mean of the untreated potential outcome equals q_U · β₀ — jointly the additive untreated-outcome (parallel-trends) model — together with a target-relevant prediction-span witness for the induced panel. Then the observed-law imputation functional identifies the target ∑ a_c · (E[Y(1) ∣ cell c] − E[Y(0) ∣ cell c]): there is an imputation-weight witness for which the population imputation functional psiImp equals the target theta.
Formal statement
Proof (Lean source)
5 supporting declarations (lemmas, instances)
-
toPanel_EY_T_eq_mean_Y1theorem — On a treated cell the observed mean equals the treated potential-outcome mean.hypothesesTreated :sharedType u_1Untreated :sharedType u_2Regressor :sharedType u_3c :Treatedconclusion(E.toPanel).EY_T c = E.cells.mean E.Y1 (inl c)Proof (Lean source)
theorem toPanel_EY_T_eq_mean_Y1 (c : Treated) : (E.toPanel).EY_T c = E.cells.mean E.Y1 (inl c) := by refine (E.cells).mean_congr_on (inl c) ?_ intro ω hω have hcell : E.cellOf ω = inl c := by simpa [cells] using hω exact E.hTreatedCons c ω hcell -
toPanel_EY_U_eq_mean_Y0theorem — On an untreated cell the observed mean equals the untreated potential-outcome mean.hypothesesTreated :sharedType u_1Untreated :sharedType u_2Regressor :sharedType u_3u :Untreatedconclusion(E.toPanel).EY_U u = E.cells.mean E.Y0 (inr u)Proof (Lean source)
theorem toPanel_EY_U_eq_mean_Y0 (u : Untreated) : (E.toPanel).EY_U u = E.cells.mean E.Y0 (inr u) := by refine (E.cells).mean_congr_on (inr u) ?_ intro ω hω have hcell : E.cellOf ω = inr u := by simpa [cells] using hω exact E.hUntreatedCons u ω hcell -
toPanel_tau_eq_po_contrasttheorem — Causal-meaning certificate. In the induced panel, tau c is literally the population treatment-effect contrast E[Y(1) ∣ cell c] − E[Y(0) ∣ cell c], so the estimand carries genuine causal content.hypothesesTreated :sharedType u_1Untreated :sharedType u_2Regressor :sharedType u_3c :TreatedProof (Lean source)
theorem toPanel_tau_eq_po_contrast (c : Treated) : (E.toPanel).tau c = E.cells.mean E.Y1 (inl c) - E.cells.mean E.Y0 (inl c) := rfl -
toPanel_treatmentEffectFixedtheorem — Treatment-effect-fixed is derived. EY_T = EY0_T + tau holds because on treated cells the observed mean is the treated potential-outcome mean and tau is the treated-minus-untreated contrast.hypothesesTreated :sharedType u_1Untreated :sharedType u_2Regressor :sharedType u_3conclusion(E.toPanel).TreatmentEffectFixedProof (Lean source)
theorem toPanel_treatmentEffectFixed : (E.toPanel).TreatmentEffectFixed := by intro c have h := E.toPanel_EY_T_eq_mean_Y1 c simp only [toPanel] at h ⊢ rw [h]; ring -
toPanel_untreatedModeltheorem — Untreated-outcome model is derived from the linear untreated-mean hypotheses plus consistency. The two linear-model conjuncts E[Y(0) ∣ cell] = q · β₀ are the genuine modeling hypotheses hLinT/hLinU (additive fixed-effect / parallel-trends form); the observed-equals-untreated conjunct is derived from untreated-cell consistency.hypothesesTreated :sharedType u_1Untreated :sharedType u_2Regressor :sharedType u_3hLinT :∀ c : Treated, E.cells.mean E.Y0 (inl c) = dot (E.qT c) E.beta0hLinU :∀ u : Untreated, E.cells.mean E.Y0 (inr u) = dot (E.qU u) E.beta0conclusion(E.toPanel).UntreatedOutcomeModelProof (Lean source)
theorem toPanel_untreatedModel (hLinT : ∀ c : Treated, E.cells.mean E.Y0 (inl c) = dot (E.qT c) E.beta0) (hLinU : ∀ u : Untreated, E.cells.mean E.Y0 (inr u) = dot (E.qU u) E.beta0) : (E.toPanel).UntreatedOutcomeModel := by refine ⟨?_, ?_, ?_⟩ · intro c; simpa [toPanel] using hLinT c · intro u; simpa [toPanel] using hLinU u · intro u rw [E.toPanel_EY_U_eq_mean_Y0 u] simp [toPanel]