Policy Margin Zero At Critical

theorem proved Hierarchy

Documentation

Lean 4 Proof

theorem policyMargin_zero_at_critical {Tstar : ℝ} :
    policyMargin Tstar Tstar = 0 := by
  simp only [policyMargin]; ring

Dependency Graph

Location

thesis/CESProofs/Hierarchy/MonetaryPolicy.lean:174

Module Section

Monetary Policy and the Liquidity Trap

In the same file

policyResponse policyResponse_nonneg policyResponse_pos_crossing liquidity_trap liquidity_trap_escape policy_ineffective_above_critical monetary_transmission_ordering institutional_amplification policyMargin policyMargin_pos_subcritical policyMargin_narrowing complementary_sectors_smaller_margin