Documentation

Lean 4 Proof

theorem monetary_transmission_ordering {J : ℕ} (hJ : 2 ≤ J)
    {ρ1 ρ2 : ℝ} (hρ : ρ1 < ρ2)
    {T_new T_old Tstar : ℝ} (hTs : 0 < Tstar) (h : T_new ≤ T_old) :
    policyResponse J ρ2 T_new T_old Tstar ≤
    policyResponse J ρ1 T_new T_old Tstar := by
  simp only [policyResponse, effectiveCurvatureKeff]
  -- Factor: K(ρ) * m_new - K(ρ) * m_old = K(ρ) * (m_new - m_old)
  rw [(mul_sub (curvatureK J ρ1) _ _).symm, (mul_sub (curvatureK J ρ2) _ _).symm]
  -- K(ρ₂) * dm ≤ K(ρ₁) * dm where dm = m_new - m_old ≥ 0
  exact mul_le_mul_of_nonneg_right
    (le_of_lt (curvatureK_decreasing_in_rho hJ hρ))
    (by linarith [degradation_monotone hTs h])

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/MonetaryPolicy.lean:115

Module Section

Monetary Policy and the Liquidity Trap

In the same file