Policy Margin Pos Subcritical

theorem proved Hierarchy

Documentation

Lean 4 Proof

theorem policyMargin_pos_subcritical {T Tstar : ℝ} (hT : T < Tstar) :
    0 < policyMargin T Tstar := by
  simp only [policyMargin]; linarith

Dependency Graph

Location

thesis/CESProofs/Hierarchy/MonetaryPolicy.lean:162

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_narrowing policyMargin_zero_at_critical complementary_sectors_smaller_margin