Documentation

Lean 4 Proof

inductive ObservableWorld where
  /-- Fast world: adjusts at v_price (electronic/information speed).
      Examples: stock prices, bond yields, credit spreads, exchange rates. -/
  | price
  /-- Slow world: adjusts at l (physical reallocation speed).
      Examples: industrial production, employment, inventories. -/
  | quantity

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/IndicatorClassification.lean:40

Module Section

Derivation of Leading and Lagging Economic Indicators

In the same file