Documentation

Lean 4 Proof

theorem liquidity_trap {J : ℕ} {ρ : ℝ}
    {T_new T_old Tstar : ℝ} (hTs : 0 < Tstar)
    (hNew : Tstar ≤ T_new) (hOld : Tstar ≤ T_old) :
    policyResponse J ρ T_new T_old Tstar = 0 := by
  simp only [policyResponse]
  rw [effectiveCurvatureKeff_above_critical J ρ T_new Tstar hTs hNew,
      effectiveCurvatureKeff_above_critical J ρ T_old Tstar hTs hOld]
  ring

Dependency Graph

Location

thesis/CESProofs/Hierarchy/MonetaryPolicy.lean:71

Module Section

Monetary Policy and the Liquidity Trap

In the same file