Documentation

Lean 4 Proof

theorem within_eliminates_fixed_effect (α_i ρ x_it x_bar_i ε_it ε_bar_i : ℝ) :
    withinTransform (panelShareIdentity α_i ρ x_it ε_it)
      (panelShareIdentity α_i ρ x_bar_i ε_bar_i) =
    ρ * withinTransform x_it x_bar_i +
    withinTransform ε_it ε_bar_i := by
  simp only [withinTransform, panelShareIdentity]; ring

Dependency Graph

Location

thesis/CESProofs/Foundations/CESEstimation.lean:295

Module Section

CES Estimation Theory: Connecting Theory to Data

In the same file