Policy Margin

def proved Hierarchy

Documentation

Lean 4 Proof

def policyMargin (T Tstar : ℝ) : ℝ := Tstar - T

Dependency Graph

Used by

policyMargin_narrowing policyMargin_pos_subcritical policyMargin_zero_at_critical complementary_sectors_smaller_margin

Location

thesis/CESProofs/Hierarchy/MonetaryPolicy.lean:159

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_pos_subcritical policyMargin_narrowing policyMargin_zero_at_critical complementary_sectors_smaller_margin