Documentation

Lean 4 Proof

theorem phillips_curve (alpha_pi alpha_y : ℝ)
    (h_pi : 0 < alpha_pi) (h_y : 0 < alpha_y) :
    -- pi = -(alpha_pi/alpha_y) * (y - y*)
    -- The Phillips curve slope is negative (determined by adjustment speed ratio)
    -(alpha_pi / alpha_y) < 0 := by
  exact neg_neg_of_pos (div_pos h_pi h_y)

Dependency Graph

Location

thesis/CESProofs/Dynamics/PhillipsCycles.lean:39

Module Section

Results 63-69: Phillips Curve, Endogenous Cycles, and Oscillation Energy

In the same file