Documentation

Lean 4 Proof

theorem phillips_flattening {J : ℕ} (hJ : 2 ≤ J) {rho_1 rho_2 C : ℝ}
    (hC : 0 < C) (hrho1 : rho_1 < 1) (_hrho2 : rho_2 < 1) (h12 : rho_1 < rho_2) :
    C * curvatureK J rho_2 < C * curvatureK J rho_1 := by
  apply mul_lt_mul_of_pos_left _ hC
  exact K_increases_with_complementarity hJ _hrho2 hrho1 h12

Dependency Graph

Location

thesis/CESProofs/Dynamics/PhillipsCycles.lean:63

Module Section

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

In the same file