Panel.Fixed­Effect

Fixed-effect projection algebra: the within transformation and its annihilator properties.

Indicator­Closed­Forms 7 core · 8 supporting · 3 submodules 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.
Fixed­Effect 3 core · 1 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.

def H_twfe reviewed
Causalean.Panel.Cells

The two-way fixed-effect subspace.

Definition (Lean source)
parameters
I :
Type u_1
shared
T :
Type u_2
shared
def
H_twfe :
Submodule ℝ (V I T)
given by
twoAxisAdditiveSpan I T
Causalean.Panel.Cells.H_twfe · Causalean/Panel/FixedEffect.lean:50 · uses V
lemma H_twfe_eq reviewed
Causalean.Panel.Cells

The two-way fixed-effect subspace H_twfe equals the generic two-axis additive span over units and periods.

Formal statement
hypotheses
I :
Type u_1
shared
T :
Type u_2
shared
conclusion
H_twfe = twoAxisAdditiveSpan I T
Proof (Lean source)
lemma H_twfe_eq : H_twfe = twoAxisAdditiveSpan I T := rfl
Causalean.Panel.Cells.H_twfe_eq · Causalean/Panel/FixedEffect.lean:59 · uses H_twfe , V , twoAxisAdditiveSpan
lemma const_mem_H_twfe reviewed
Causalean.Panel.Cells

For any constant c₀, the constant array c₀ belongs to the two-way fixed-effect subspace H_twfe.

Formal statement
hypotheses
I :
Type u_1
shared
T :
Type u_2
shared
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₀
Causalean.Panel.Cells.const_mem_H_twfe · Causalean/Panel/FixedEffect.lean:64 · uses H_twfe , V
1 supporting declaration (lemmas, instances)
  • H_twfe_finiteDimensional instance — H_twfe is finite-dimensional: inherits from AdditiveSpan.finiteDimensional.
    parameters
    I :
    Type u_1
    shared
    T :
    Type u_2
    shared
    instance
    H_twfe_finiteDimensional :
    Finite ℝ (H_twfe (I := I) (T := T))
    given by
    finiteDimensional
    Causalean.Panel.Cells.H_twfe_finiteDimensional · Causalean/Panel/FixedEffect.lean:74