Documentation

Lean 4 Proof

theorem policyResponse_pos_crossing {J : ℕ} (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {T_new T_old Tstar : ℝ} (hTs : 0 < Tstar)
    (hNew_nn : 0 ≤ T_new) (hNew : T_new < Tstar) (hOld : Tstar ≤ T_old) :
    0 < policyResponse J ρ T_new T_old Tstar := by
  simp only [policyResponse]
  rw [effectiveCurvatureKeff_above_critical J ρ T_old Tstar hTs hOld]
  simp only [sub_zero]
  exact effectiveCurvatureKeff_pos hJ hρ hNew_nn hTs hNew

Dependency Graph

Location

thesis/CESProofs/Hierarchy/MonetaryPolicy.lean:51

Module Section

Monetary Policy and the Liquidity Trap

In the same file