Documentation

Lean 4 Proof

inductive ObservableEigenspace where
  /-- Projects onto 1-perp: relative/differential observable.
      Carries curvature information; K-sensitivity = (1-rho)(J-1)/J > 0.
      Examples: price spreads, cross-sector correlations, return dispersion. -/
  | relative
  /-- Projects onto span(1): aggregate/level observable.
      rho-invariant at symmetry; K-sensitivity = 0.
      Examples: GDP, aggregate CPI level, total employment. -/
  | aggregate

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/IndicatorClassification.lean:50

Module Section

Derivation of Leading and Lagging Economic Indicators

In the same file