Documentation

Lean 4 Proof

theorem policy_ineffective_above_critical {J : ℕ} {ρ : ℝ}
    {T Tstar : ℝ} (hTs : 0 < Tstar) (hT : Tstar ≤ T) :
    effectiveCurvatureKeff J ρ T Tstar = 0 :=
  effectiveCurvatureKeff_above_critical J ρ T Tstar hTs hT

Dependency Graph

Location

thesis/CESProofs/Hierarchy/MonetaryPolicy.lean:95

Module Section

Monetary Policy and the Liquidity Trap

In the same file