Documentation

Lean 4 Proof

theorem complementary_sectors_smaller_margin {J : ℕ} (hJ : 2 ≤ J)
    {ρ1 ρ2 : ℝ} (hρ1 : ρ1 < 1) (hρ2 : ρ2 < 1) (hρ : ρ1 < ρ2)
    {c d_sq : ℝ} (hc : 0 < c) (hd : 0 < d_sq) :
    policyMargin T (criticalFriction J ρ1 c d_sq) <
    policyMargin T (criticalFriction J ρ2 c d_sq) := by
  simp only [policyMargin]
  linarith [complementary_goods_more_fragile hJ hρ1 hρ2 hρ hc hd]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/MonetaryPolicy.lean:186

Module Section

Monetary Policy and the Liquidity Trap

In the same file