Panel.FixedEffect
Fixed-effect projection algebra: the within transformation and its annihilator properties.
FixedEffect 2 core · 0 supporting This file defines the two-way fixed-effect subspace of panel arrays as the set of unit-plus-period additive functions. ★ H_twfe_eq★ const_mem_H_twfe
Two-Way Fixed Effects
This file defines the two-way fixed-effect subspace of panel arrays as the set of unit-plus-period additive functions. It connects the panel notation to the generic additive-span infrastructure and records basic membership and finite-dimensionality facts.
lemma H_twfe_eq reviewed
⚑ flagged
Causalean.Panel.Cells
The two-way fixed-effect subspace H_twfe equals the generic two-axis additive span over units and periods.
Formal statement
conclusion
H_twfe = twoAxisAdditiveSpan I T
Proof (Lean source)
lemma H_twfe_eq :
H_twfe = twoAxisAdditiveSpan I T := rfl
lemma const_mem_H_twfe reviewed
⚑ flagged
Causalean.Panel.Cells
For any constant c₀, the constant array c₀ belongs to the two-way fixed-effect subspace H_twfe.
Formal statement
hypotheses
c₀ :
ℝ
conclusion
(fun _ : I × T => c₀) ∈ H_twfe
Proof (Lean source)
lemma const_mem_H_twfe (c₀ : ℝ) :
(fun _ : I × T => c₀) ∈ H_twfe :=
const_mem (Prod.fst : I × T → I) snd c₀
IndicatorClosedForms 6 core · 7 supporting This file proves closed-form two-way fixed-effect residuals for structured indicator arrays, including unit-only, period-only, rectangular, cohort-period, diagonal, and triangular indicators. ★ H_twfe_orthogonal_iff★ tildeX_product_indicator_balanced★ tildeX_cell_indicator_cohortPeriod★ tildeX_diagonal_indicator_cohortPeriod★ tildeX_triangular_indicator_cohortPeriod
Indicator Residual Closed Forms
This file proves closed-form two-way fixed-effect residuals for structured
indicator arrays, including unit-only, period-only, rectangular, cohort-period,
diagonal, and triangular indicators. It also provides the exported
row-and-column orthogonality criterion H_twfe_orthogonal_iff, the finite
cohort law CohortLaw, and the generic cohort-period weighted panel
construction cohortPeriodCells, so downstream files can reuse the algebra
without importing a specialized regression instance.
lemma H_twfe_orthogonal_iff reviewed
⚑ flagged
Causalean.Panel.Cells
For a panel weighting scheme and any panel array g, g is orthogonal, under the weighted inner product, to every member of the two-way fixed-effect subspace H_twfe exactly when it is orthogonal to every unit indicator and every period indicator.
Formal statement
hypotheses
c :
Cells I T
g :
V I T
conclusion
(∀ h ∈ Cells.H_twfe, c.ip g h = 0)
↔ ((∀ i₀ : I, c.ip g (fun r => if r.1 = i₀ then (1 : ℝ) else 0) = 0) ∧ (∀ t₀ : T, c.ip g (fun r => if r.2 = t₀ then (1 : ℝ) else 0) = 0))
Proof (Lean source)
lemma H_twfe_orthogonal_iff (c : Cells I T) (g : V I T) :
(∀ h ∈ Cells.H_twfe, c.ip g h = 0) ↔
((∀ i₀ : I,
c.ip g (fun r => if r.1 = i₀ then (1 : ℝ) else 0) = 0) ∧
(∀ t₀ : T,
c.ip g (fun r => if r.2 = t₀ then (1 : ℝ) else 0) = 0)) := by
classical
constructor
· intro horth
constructor
· intro i₀
exact horth (fun r => if r.1 = i₀ then (1 : ℝ) else 0)
⟨fun i => if i = i₀ then (1 : ℝ) else 0, fun _ => 0,
by intro p; simp⟩
· intro t₀
exact horth (fun r => if r.2 = t₀ then (1 : ℝ) else 0)
⟨fun _ => 0, fun t => if t = t₀ then (1 : ℝ) else 0,
by intro p; simp⟩
· rintro ⟨hunit, hperiod⟩ h ⟨a, b, hh⟩
have hA :
c.ip g (fun r : I × T => a r.1) = 0 := by
have hexp :
c.ip g (fun r : I × T => a r.1) =
∑ i₀ : I, a i₀ *
c.ip g (fun r : I × T => if r.1 = i₀ then (1 : ℝ) else 0) := by
unfold ip
rw [show
(∑ i₀ : I, a i₀ *
∑ x ∈ c.observed,
c.weight x * g x * (if x.1 = i₀ then (1 : ℝ) else 0)) =
∑ x ∈ c.observed, c.weight x * g x * a x.1 by
rw [show
(∑ i₀ : I, a i₀ *
∑ x ∈ c.observed,
c.weight x * g x * (if x.1 = i₀ then (1 : ℝ) else 0)) =
∑ i₀ : I, ∑ x ∈ c.observed,
a i₀ * (c.weight x * g x * (if x.1 = i₀ then (1 : ℝ) else 0)) by
refine Finset.sum_congr rfl ?_
intro i₀ _
rw [Finset.mul_sum]]
rw [Finset.sum_comm]
refine Finset.sum_congr rfl ?_
intro x hx
rw [show
(∑ i₀ : I,
a i₀ * (c.weight x * g x * (if x.1 = i₀ then (1 : ℝ) else 0))) =
c.weight x * g x * a x.1 by
rw [show
(∑ i₀ : I,
a i₀ * (c.weight x * g x * (if x.1 = i₀ then (1 : ℝ) else 0))) =
(c.weight x * g x) *
∑ i₀ : I, a i₀ * (if x.1 = i₀ then (1 : ℝ) else 0) by
rw [Finset.mul_sum]
refine Finset.sum_congr rfl ?_
intro i₀ _
ring]
rw [show (∑ i₀ : I, a i₀ * (if x.1 = i₀ then (1 : ℝ) else 0)) =
a x.1 by
rw [Finset.sum_eq_single x.1]
· simp
· intro y _ hy
simp [hy.symm]
· intro hnot
exact (hnot (Finset.mem_univ x.1)).elim]
]]
rw [hexp]
exact Finset.sum_eq_zero (fun i₀ _ => by rw [hunit i₀, mul_zero])
have hB :
c.ip g (fun r : I × T => b r.2) = 0 := by
have hexp :
c.ip g (fun r : I × T => b r.2) =
∑ t₀ : T, b t₀ *
c.ip g (fun r : I × T => if r.2 = t₀ then (1 : ℝ) else 0) := by
unfold ip
rw [show
(∑ t₀ : T, b t₀ *
∑ x ∈ c.observed,
c.weight x * g x * (if x.2 = t₀ then (1 : ℝ) else 0)) =
∑ x ∈ c.observed, c.weight x * g x * b x.2 by
rw [show
(∑ t₀ : T, b t₀ *
∑ x ∈ c.observed,
c.weight x * g x * (if x.2 = t₀ then (1 : ℝ) else 0)) =
∑ t₀ : T, ∑ x ∈ c.observed,
b t₀ * (c.weight x * g x * (if x.2 = t₀ then (1 : ℝ) else 0)) by
refine Finset.sum_congr rfl ?_
intro t₀ _
rw [Finset.mul_sum]]
rw [Finset.sum_comm]
refine Finset.sum_congr rfl ?_
intro x hx
rw [show
(∑ t₀ : T,
b t₀ * (c.weight x * g x * (if x.2 = t₀ then (1 : ℝ) else 0))) =
c.weight x * g x * b x.2 by
rw [show
(∑ t₀ : T,
b t₀ * (c.weight x * g x * (if x.2 = t₀ then (1 : ℝ) else 0))) =
(c.weight x * g x) *
∑ t₀ : T, b t₀ * (if x.2 = t₀ then (1 : ℝ) else 0) by
rw [Finset.mul_sum]
refine Finset.sum_congr rfl ?_
intro t₀ _
ring]
rw [show (∑ t₀ : T, b t₀ * (if x.2 = t₀ then (1 : ℝ) else 0)) =
b x.2 by
rw [Finset.sum_eq_single x.2]
· simp
· intro y _ hy
simp [hy.symm]
· intro hnot
exact (hnot (Finset.mem_univ x.2)).elim]
]]
rw [hexp]
exact Finset.sum_eq_zero (fun t₀ _ => by rw [hperiod t₀, mul_zero])
calc
c.ip g h = c.ip g ((fun r : I × T => a r.1) + fun r : I × T => b r.2) := by
congr 1
ext p
exact hh p
_ = c.ip g (fun r : I × T => a r.1) +
c.ip g (fun r : I × T => b r.2) := by
rw [c.ip_add_right]
_ = 0 := by rw [hA, hB]; ring
theorem tildeX_product_indicator_balanced reviewed
⚑ flagged
Causalean.Panel.Cells
For a subset of units S_I, a subset of periods S_T, and an evaluation cell r, under balanced (equal) weights, the two-way-fixed-effect residual of the product indicator 1{i ∈ S_I}·1{t ∈ S_T}, evaluated at r, factorizes into the product of the centered unit indicator and the centered period indicator.
Formal statement
hypotheses
conclusion
(balanced (I := I) (T := T)).tildeX Cells.H_twfe (fun s : I × T => (if s.1 ∈ S_I then (1 : ℝ) else 0) * (if s.2 ∈ S_T then (1 : ℝ) else 0)) r
= ((if r.1 ∈ S_I then (1 : ℝ) else 0) - (S_I.card : ℝ) / (Fintype.card I : ℝ)) * ((if r.2 ∈ S_T then (1 : ℝ) else 0) - (S_T.card : ℝ) / (Fintype.card T : ℝ))
Proof (Lean source)
theorem tildeX_product_indicator_balanced (S_I : Finset I) (S_T : Finset T)
(r : I × T) :
(balanced (I := I) (T := T)).tildeX
Cells.H_twfe
(fun s : I × T =>
(if s.1 ∈ S_I then (1 : ℝ) else 0) *
(if s.2 ∈ S_T then (1 : ℝ) else 0)) r =
((if r.1 ∈ S_I then (1 : ℝ) else 0) -
(S_I.card : ℝ) / (Fintype.card I : ℝ)) *
((if r.2 ∈ S_T then (1 : ℝ) else 0) -
(S_T.card : ℝ) / (Fintype.card T : ℝ)) := by
classical
let c : Cells I T := balanced (I := I) (T := T)
let X : V I T := fun s : I × T =>
(if s.1 ∈ S_I then (1 : ℝ) else 0) *
(if s.2 ∈ S_T then (1 : ℝ) else 0)
let Y : V I T := fun s : I × T =>
((if s.1 ∈ S_I then (1 : ℝ) else 0) -
(S_I.card : ℝ) / (Fintype.card I : ℝ)) *
((if s.2 ∈ S_T then (1 : ℝ) else 0) -
(S_T.card : ℝ) / (Fintype.card T : ℝ))
let G : V I T := X - Y
have hG_mem : G ∈ Cells.H_twfe := by
refine ⟨fun i =>
((S_T.card : ℝ) / (Fintype.card T : ℝ)) *
(if i ∈ S_I then (1 : ℝ) else 0),
fun t =>
((S_I.card : ℝ) / (Fintype.card I : ℝ)) *
(if t ∈ S_T then (1 : ℝ) else 0) -
((S_I.card : ℝ) / (Fintype.card I : ℝ)) *
((S_T.card : ℝ) / (Fintype.card T : ℝ)), ?_⟩
intro p
by_cases hi : p.1 ∈ S_I <;> by_cases ht : p.2 ∈ S_T <;> simp [G, X, Y, hi, ht] <;>
ring
have hXsubG : X - G = Y := by
ext s
simp [G]
have horth : ∀ h ∈ Cells.H_twfe, c.ip (X - G) h = 0 := by
rw [H_twfe_orthogonal_iff]
constructor
· intro i₀
rw [hXsubG]
simpa [c, Y] using balanced_centered_product_orth_unit (S_I := S_I) (S_T := S_T) i₀
· intro t₀
rw [hXsubG]
simpa [c, Y] using balanced_centered_product_orth_period (S_I := S_I) (S_T := S_T) t₀
have hproj : c.proj Cells.H_twfe X r = G r :=
c.proj_apply_eq_of_mem_orthogonal Cells.H_twfe X hG_mem horth r (by simp [c])
calc
c.tildeX Cells.H_twfe X r = (X - c.proj Cells.H_twfe X) r := by simp [Cells.tildeX_eq]
_ = Y r := by
rw [Pi.sub_apply, hproj]
exact congrFun hXsubG r
_ = ((if r.1 ∈ S_I then (1 : ℝ) else 0) -
(S_I.card : ℝ) / (Fintype.card I : ℝ)) *
((if r.2 ∈ S_T then (1 : ℝ) else 0) -
(S_T.card : ℝ) / (Fintype.card T : ℝ)) := rfl
structure CohortLaw reviewed
⚑ flagged
Causalean.Panel.Cells
Cohort law on a finite cohort index Fin C: probabilities π(g) ≥ 0 summing to one.
theorem tildeX_cell_indicator_cohortPeriod reviewed
⚑ flagged
Causalean.Panel.Cells
For a target cohort g₀, a target period t₀, and an evaluation cell r, the cohort-period-weighted two-way-fixed-effect residual of the cell indicator 1{g = g₀, t = t₀}, evaluated at r, equals the product of centered cohort and period indicators minus the corresponding cross terms fixed by the gauge normalization ∑_t β(t) = π(g₀).
Formal statement
Proof (Lean source)
theorem tildeX_cell_indicator_cohortPeriod (g₀ : Fin C) (t₀ : Fin S)
(r : Fin C × Fin S) :
(cohortPeriodCells law hpi).tildeX
Cells.H_twfe
(fun s : Fin C × Fin S =>
if s.1 = g₀ ∧ s.2 = t₀ then (1 : ℝ) else 0) r =
(if r.1 = g₀ then (1 : ℝ) else 0) *
(if r.2 = t₀ then (1 : ℝ) else 0)
- (law.pi g₀ : ℝ) * (if r.2 = t₀ then (1 : ℝ) else 0)
- (1 / (card (Fin S) : ℝ)) *
(if r.1 = g₀ then (1 : ℝ) else 0)
+ (law.pi g₀ : ℝ) / (card (Fin S) : ℝ) := by
classical
let c : Cells (Fin C) (Fin S) := cohortPeriodCells law hpi
let X : V (Fin C) (Fin S) := fun s : Fin C × Fin S =>
if s.1 = g₀ ∧ s.2 = t₀ then (1 : ℝ) else 0
let Y : V (Fin C) (Fin S) := fun s : Fin C × Fin S =>
((if s.1 = g₀ then (1 : ℝ) else 0) - (law.pi g₀ : ℝ)) *
((if s.2 = t₀ then (1 : ℝ) else 0) -
1 / (card (Fin S) : ℝ))
let G : V (Fin C) (Fin S) := X - Y
have hG_mem : G ∈ Cells.H_twfe := by
refine ⟨fun g => (1 / (card (Fin S) : ℝ)) *
(if g = g₀ then (1 : ℝ) else 0),
fun t => (law.pi g₀ : ℝ) * (if t = t₀ then (1 : ℝ) else 0) -
(law.pi g₀ : ℝ) / (card (Fin S) : ℝ), ?_⟩
intro p
by_cases hg : p.1 = g₀ <;> by_cases ht : p.2 = t₀ <;>
simp [G, X, Y, hg, ht] <;> ring
have hXsubG : X - G = Y := by
ext s
simp [G]
have horth : ∀ h ∈ Cells.H_twfe, c.ip (X - G) h = 0 := by
rw [H_twfe_orthogonal_iff]
constructor
· intro g₁
rw [hXsubG]
simpa [c, Y] using
cohort_cell_centered_orth_unit (law := law) (hpi := hpi) (g₀ := g₀)
(g₁ := g₁) (t₀ := t₀)
· intro t₁
rw [hXsubG]
simpa [c, Y] using
cohort_cell_centered_orth_period (law := law) (hpi := hpi) (g₀ := g₀)
(t₀ := t₀) (t₁ := t₁)
have hproj : c.proj Cells.H_twfe X r = G r :=
c.proj_apply_eq_of_mem_orthogonal Cells.H_twfe X hG_mem horth r
(by simp [c, cohortPeriodCells])
calc
c.tildeX Cells.H_twfe X r = (X - c.proj Cells.H_twfe X) r := by simp [Cells.tildeX_eq]
_ = Y r := by
rw [Pi.sub_apply, hproj]
exact congrFun hXsubG r
_ = (if r.1 = g₀ then (1 : ℝ) else 0) *
(if r.2 = t₀ then (1 : ℝ) else 0)
- (law.pi g₀ : ℝ) * (if r.2 = t₀ then (1 : ℝ) else 0)
- (1 / (card (Fin S) : ℝ)) *
(if r.1 = g₀ then (1 : ℝ) else 0)
+ (law.pi g₀ : ℝ) / (card (Fin S) : ℝ) := by
by_cases hg : r.1 = g₀ <;> by_cases ht : r.2 = t₀ <;>
simp [Y, hg, ht] <;> ring
theorem tildeX_diagonal_indicator_cohortPeriod reviewed
⚑ flagged
Causalean.Panel.Cells
For an evaluation cell r, the cohort-period-weighted two-way-fixed-effect residual of the diagonal (switch-on) indicator 1{g.val = t.val}, evaluated at r, equals the indicator minus the cohort-conditional mean, minus the period-conditional mean net of the grand mean.
Formal statement
Proof (Lean source)
theorem tildeX_diagonal_indicator_cohortPeriod
(r : Fin C × Fin S) :
(cohortPeriodCells law hpi).tildeX
Cells.H_twfe
(fun s : Fin C × Fin S => if s.1.val = s.2.val then (1 : ℝ) else 0) r =
(if r.1.val = r.2.val then (1 : ℝ) else 0)
- (if r.1.val < S then 1 / (card (Fin S) : ℝ) else 0)
- (if h : r.2.val < C then (law.pi ⟨r.2.val, h⟩ : ℝ) else 0)
+ (1 / (card (Fin S) : ℝ)) *
∑ g : Fin C, (if g.val < S then (law.pi g : ℝ) else 0) := by
classical
let c : Cells (Fin C) (Fin S) := cohortPeriodCells law hpi
let X : V (Fin C) (Fin S) := diagX
let Y : V (Fin C) (Fin S) := diagY law
let G : V (Fin C) (Fin S) := X - Y
have hG_mem : G ∈ Cells.H_twfe := by
refine ⟨fun g => diagRowMean (S := S) g - diagGrandMean (S := S) law,
fun t => diagPeriodMean law t, ?_⟩
intro p
simp [G, X, Y, diagY, diagX, diagRowMean, diagPeriodMean, diagGrandMean]
ring
have hXsubG : X - G = Y := by
ext s
simp [G]
have horth : ∀ h ∈ Cells.H_twfe, c.ip (X - G) h = 0 := by
rw [H_twfe_orthogonal_iff]
constructor
· intro g₁
rw [hXsubG]
exact diagonal_centered_orth_unit (S := S) (law := law) (hpi := hpi) (g₁ := g₁)
· intro t₁
rw [hXsubG]
exact diagonal_centered_orth_period (S := S) (law := law) (hpi := hpi) (t₁ := t₁)
have hproj : c.proj Cells.H_twfe X r = G r :=
c.proj_apply_eq_of_mem_orthogonal Cells.H_twfe X hG_mem horth r
(by simp [c, cohortPeriodCells])
calc
c.tildeX Cells.H_twfe X r = (X - c.proj Cells.H_twfe X) r := by
simp [Cells.tildeX_eq]
_ = Y r := by
rw [Pi.sub_apply, hproj]
exact congrFun hXsubG r
_ = (if r.1.val = r.2.val then (1 : ℝ) else 0)
- (if r.1.val < S then 1 / (card (Fin S) : ℝ) else 0)
- (if h : r.2.val < C then (law.pi ⟨r.2.val, h⟩ : ℝ) else 0)
+ (1 / (card (Fin S) : ℝ)) *
∑ g : Fin C, (if g.val < S then (law.pi g : ℝ) else 0) := rfl
theorem tildeX_triangular_indicator_cohortPeriod reviewed
⚑ flagged
Causalean.Panel.Cells
For an evaluation cell r, the cohort-period-weighted two-way-fixed-effect residual of the triangular (continued-treatment) indicator 1{g.val < t.val}, evaluated at r, equals the indicator minus the cohort-conditional mean, minus the period-conditional mean net of the grand mean.
Formal statement
Proof (Lean source)
theorem tildeX_triangular_indicator_cohortPeriod
(r : Fin C × Fin S) :
(cohortPeriodCells law hpi).tildeX
Cells.H_twfe
(fun s : Fin C × Fin S => if s.1.val < s.2.val then (1 : ℝ) else 0) r =
(if r.1.val < r.2.val then (1 : ℝ) else 0)
- (∑ s : Fin S, (if r.1.val < s.val then (1 : ℝ) else 0)) /
(card (Fin S) : ℝ)
- (∑ g : Fin C,
(if g.val < r.2.val then (1 : ℝ) else 0) * (law.pi g : ℝ))
+ (1 / (card (Fin S) : ℝ)) *
∑ g : Fin C, ∑ s : Fin S,
(if g.val < s.val then (law.pi g : ℝ) else 0) := by
classical
let c : Cells (Fin C) (Fin S) := cohortPeriodCells law hpi
let X : V (Fin C) (Fin S) := triX
let Y : V (Fin C) (Fin S) := triY law
let G : V (Fin C) (Fin S) := X - Y
have hG_mem : G ∈ Cells.H_twfe := by
refine ⟨fun g => triRowMean (S := S) g - triGrandMean (S := S) law,
fun t => triPeriodMean law t, ?_⟩
intro p
simp [G, X, Y, triY, triX, triRowMean, triPeriodMean, triGrandMean]
ring
have hXsubG : X - G = Y := by
ext s
simp [G]
have horth : ∀ h ∈ Cells.H_twfe, c.ip (X - G) h = 0 := by
rw [H_twfe_orthogonal_iff]
constructor
· intro g₁
rw [hXsubG]
exact tri_centered_orth_unit (S := S) (law := law) (hpi := hpi) (g₁ := g₁)
· intro t₁
rw [hXsubG]
exact tri_centered_orth_period (S := S) (law := law) (hpi := hpi) (t₁ := t₁)
have hproj : c.proj Cells.H_twfe X r = G r :=
c.proj_apply_eq_of_mem_orthogonal Cells.H_twfe X hG_mem horth r
(by simp [c, cohortPeriodCells])
calc
c.tildeX Cells.H_twfe X r = (X - c.proj Cells.H_twfe X) r := by
simp [Cells.tildeX_eq]
_ = Y r := by
rw [Pi.sub_apply, hproj]
exact congrFun hXsubG r
_ = (if r.1.val < r.2.val then (1 : ℝ) else 0)
- (∑ s : Fin S, (if r.1.val < s.val then (1 : ℝ) else 0)) /
(card (Fin S) : ℝ)
- (∑ g : Fin C,
(if g.val < r.2.val then (1 : ℝ) else 0) * (law.pi g : ℝ))
+ (1 / (card (Fin S) : ℝ)) *
∑ g : Fin C, ∑ s : Fin S,
(if g.val < s.val then (law.pi g : ℝ) else 0) := rfl
7 supporting declarations (lemmas, instances)
-
sum_centered_indicator_mem_reallemma — Centering the indicator of a finite subset by its uniform average makes its sum across the index set equal to zero.hypothesesα :S :Finset αconclusion(∑ x : α, ((if x ∈ S then (1 : ℝ) else 0) - (S.card : ℝ) / (Fintype.card α : ℝ))) = 0Proof (Lean source)
lemma sum_centered_indicator_mem_real {α : Type*} [Fintype α] [DecidableEq α] (S : Finset α) : (∑ x : α, ((if x ∈ S then (1 : ℝ) else 0) - (S.card : ℝ) / (Fintype.card α : ℝ))) = 0 := by rcases isEmpty_or_nonempty α with hα | hα · letI := hα simp · letI := hα rw [Finset.sum_sub_distrib, sum_indicator_mem_real] rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul] have hcard : (Fintype.card α : ℝ) ≠ 0 := by have : 0 < Fintype.card α := Fintype.card_pos exact_mod_cast this.ne' field_simp [hcard] ring -
tildeX_consttheorem — The TWFE residual of a constant array vanishes on every observed cell.hypothesesconclusionc.tildeX Cells.H_twfe (fun _ : I × T => k) r = 0Proof (Lean source)
theorem tildeX_const (c : Cells I T) (k : ℝ) (r : I × T) (hr : r ∈ c.observed) : c.tildeX Cells.H_twfe (fun _ : I × T => k) r = 0 := by -- PROOF: constants belong to `H_twfe` (`const_mem_H_twfe`), so by -- `residualize_self_of_mem` the residual vanishes on observed cells. exact c.residualize_self_of_mem Cells.H_twfe (Cells.const_mem_H_twfe k) r hr -
tildeX_unit_indicatortheorem — Unit indicator is absorbed by H_twfe: ind(i = i₀) lies in H_twfe (via a(i) := ind(i = i₀), b(t) := 0), so its residual vanishes on every observed cell. Independent of the weights.hypothesesconclusionc.tildeX Cells.H_twfe (fun s : I × T => if s.1 = i₀ then (1 : ℝ) else 0) r = 0Proof (Lean source)
theorem tildeX_unit_indicator (c : Cells I T) (i₀ : I) (r : I × T) (hr : r ∈ c.observed) : c.tildeX Cells.H_twfe (fun s : I × T => if s.1 = i₀ then (1 : ℝ) else 0) r = 0 := by apply c.residualize_self_of_mem Cells.H_twfe ?_ r hr exact ⟨fun i => (if i = i₀ then 1 else 0 : ℝ), fun _ => 0, by intro p; simp⟩ -
tildeX_period_indicatortheorem — Period indicator is absorbed by H_twfe: ind(t = t₀) lies in H_twfe (via a := 0, b(t) := ind(t = t₀)), so its residual vanishes on every observed cell. Independent of the weights.hypothesesconclusionc.tildeX Cells.H_twfe (fun s : I × T => if s.2 = t₀ then (1 : ℝ) else 0) r = 0Proof (Lean source)
theorem tildeX_period_indicator (c : Cells I T) (t₀ : T) (r : I × T) (hr : r ∈ c.observed) : c.tildeX Cells.H_twfe (fun s : I × T => if s.2 = t₀ then (1 : ℝ) else 0) r = 0 := by apply c.residualize_self_of_mem Cells.H_twfe ?_ r hr exact ⟨fun _ => 0, fun t => (if t = t₀ then 1 else 0 : ℝ), by intro p; simp⟩ -
cohort_sum_pi_centered_eq_zerolemma — A singleton indicator centered by the selected category's weight has a zero weighted average whenever the weights across categories sum to one.hypothesesconclusion(∑ g : α, w g * ((if g = g₀ then (1 : ℝ) else 0) - w g₀)) = 0Proof (Lean source)
lemma cohort_sum_pi_centered_eq_zero {α : Type*} [Fintype α] [DecidableEq α] (w : α → ℝ) (hw : ∑ g, w g = 1) (g₀ : α) : (∑ g : α, w g * ((if g = g₀ then (1 : ℝ) else 0) - w g₀)) = 0 := by rw [show (∑ g : α, w g * ((if g = g₀ then (1 : ℝ) else 0) - w g₀)) = (∑ g : α, w g * (if g = g₀ then (1 : ℝ) else 0)) - ∑ g : α, w g * w g₀ by rw [← Finset.sum_sub_distrib] refine Finset.sum_congr rfl ?_ intro g hg ring] rw [show (∑ x : α, w x * if x = g₀ then 1 else 0) = w g₀ by simpa [mul_comm] using (Fintype.sum_ite_eq (i := g₀) (f := fun g : α => w g)).symm] rw [show (∑ g : α, w g * w g₀) = (∑ g : α, w g) * w g₀ by rw [Finset.sum_mul]] rw [hw] ring -
cohortPeriod_ip_unit_eqlemma — In a cohort-by-period panel with cohort-period weights, the weighted inner product of any outcome array with a cohort's unit indicator equals that cohort's weighted sum of outcomes across periods.hypothesesProof (Lean source)
lemma cohortPeriod_ip_unit_eq (law : CohortLaw C) (hpi : ∀ g : Fin C, 0 < (law.pi g : ℝ)) (Y : V (Fin C) (Fin S)) (g₁ : Fin C) : (cohortPeriodCells law hpi).ip Y (fun r : Fin C × Fin S => if r.1 = g₁ then (1 : ℝ) else 0) = ((law.pi g₁ : ℝ) / (card (Fin S) : ℝ)) * ∑ t : Fin S, Y (g₁, t) := by unfold ip simp only [cohortPeriodCells, Finset.mem_univ, ite_mul, one_mul, zero_mul, mul_ite, mul_one, mul_zero, ↓reduceIte] rw [Fintype.sum_prod_type] rw [show (∑ x : Fin C, ∑ t : Fin S, if x = g₁ then (law.pi x : ℝ) / (card (Fin S) : ℝ) * Y (x, t) else 0) = ∑ t : Fin S, (law.pi g₁ : ℝ) / (card (Fin S) : ℝ) * Y (g₁, t) by simpa [eq_comm] using (Fintype.sum_ite_eq (i := g₁) (f := fun x : Fin C => ∑ t : Fin S, (law.pi x : ℝ) / (card (Fin S) : ℝ) * Y (x, t))).symm] rw [Finset.mul_sum] -
cohortPeriod_ip_period_eqlemma — In a cohort-by-period panel with cohort-period weights, the weighted inner product of any outcome array with a period indicator equals the cohort-weighted sum of outcomes in that period.hypothesesProof (Lean source)
lemma cohortPeriod_ip_period_eq (law : CohortLaw C) (hpi : ∀ g : Fin C, 0 < (law.pi g : ℝ)) (Y : V (Fin C) (Fin S)) (t₁ : Fin S) : (cohortPeriodCells law hpi).ip Y (fun r : Fin C × Fin S => if r.2 = t₁ then (1 : ℝ) else 0) = (1 / (card (Fin S) : ℝ)) * ∑ g : Fin C, (law.pi g : ℝ) * Y (g, t₁) := by unfold ip simp only [cohortPeriodCells, Finset.mem_univ, ite_mul, one_mul, zero_mul, mul_ite, mul_one, mul_zero, ↓reduceIte] rw [Fintype.sum_prod_type] rw [show (∑ g : Fin C, ∑ t : Fin S, if t = t₁ then (law.pi g : ℝ) / (card (Fin S) : ℝ) * Y (g, t) else 0) = ∑ g : Fin C, (law.pi g : ℝ) / (card (Fin S) : ℝ) * Y (g, t₁) by refine Finset.sum_congr rfl ?_ intro g _ simpa [eq_comm] using (Fintype.sum_ite_eq (i := t₁) (f := fun t : Fin S => (law.pi g : ℝ) / (card (Fin S) : ℝ) * Y (g, t))).symm] rw [Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro g _ ring