Sections / Section 12: Two-World Economy and Indicators / aggregate_has_zero_K_sensitivity

Aggregate Has Zero K Sensitivity

theoremprovedDynamics & Crises

Documentation

Lean 4 Proof

theorem aggregate_has_zero_K_sensitivity {J : ℕ} :
    curvatureK J 1 = 0 :=
  curvatureK_eq_zero_of_rho_one

Dependency Graph

Location

thesis/CESProofs/Dynamics/IndicatorClassification.lean:112

Module Section

Derivation of Leading and Lagging Economic Indicators

In the same file

ObservableWorld ObservableEigenspace TemporalType IndicatorProfile relative_has_positive_K_sensitivity flow_positive_implies_stock_rising flow_decline_while_stock_rises administeredSpeed marketClearing_full_speed administered_slower administered_relaxTime_gt indicator_classification_foundations spIndex yieldCurveSpread ismNewOrders initialClaims avgWeeklyHours industrialProduction nonfarmPayrolls personalIncome