Documentation

Lean 4 Proof

theorem policyResponse_nonneg {J : ℕ} (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {T_new T_old Tstar : ℝ} (hTs : 0 < Tstar) (h : T_new ≤ T_old) :
    0 ≤ policyResponse J ρ T_new T_old Tstar := by
  simp only [policyResponse]
  linarith [bilateral_Keff_decreasing hJ hρ hTs h]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/MonetaryPolicy.lean:41

Module Section

Monetary Policy and the Liquidity Trap

In the same file