Documentation

Lean 4 Proof

theorem liquidity_trap_escape {J : ℕ} (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {T Tstar : ℝ} (hTs : 0 < Tstar) (hT_nn : 0 ≤ T) (hT : T < Tstar) :
    0 < effectiveCurvatureKeff J ρ T Tstar :=
  effectiveCurvatureKeff_pos hJ hρ hT_nn hTs hT

Dependency Graph

Location

thesis/CESProofs/Hierarchy/MonetaryPolicy.lean:87

Module Section

Monetary Policy and the Liquidity Trap

In the same file