Panel.Estimand­Characterization.Imputation­Event­Study

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

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

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

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

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

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]

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 _ _

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

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

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]

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

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 := Classical.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

theorem treated_or_untreated (c : I × Fin T) : AdoptionPath.le (g c.1) c.2 ∨ AdoptionPath.lt (g c.1) c.2 := by unfold AdoptionPath.le AdoptionPath.lt rcases lt_trichotomy (g c.1) (c.2 : WithTop (Fin T)) with h | h | h · exact inl (le_of_lt h) · exact inl (le_of_eq h) · exact inr h

lemma dot_feRow (c : I × Fin T) (α : I → ℝ) (lam : Fin T → ℝ) : dot (feRow c) (elim α lam) = α c.1 + lam c.2 := by unfold dot feRow rw [Fintype.sum_sum_type] simp only [Sum.elim_inl, Sum.elim_inr, ite_mul, one_mul, zero_mul, Finset.sum_ite_eq', Finset.mem_univ, if_true]

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

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

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

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]