Documentation

Lean 4 Proof

theorem institutions_dampen_spillover {J : ℕ} (hJ : 2 ≤ J)
    {ρ : ℝ} (hρ : ρ < 1)
    {T Tstar1 Tstar2 : ℝ} (hTs1 : 0 < Tstar1) (hTs2 : 0 < Tstar2)
    (h : Tstar1 ≤ Tstar2) (hT : 0 ≤ T) :
    effectiveCurvatureKeff J ρ T Tstar1 ≤ effectiveCurvatureKeff J ρ T Tstar2 :=
  institutional_amplification hJ hρ hTs1 hTs2 h hT

Dependency Graph

Location

thesis/CESProofs/Applications/OpenEconomy.lean:146

Module Section

Open Economy Monetary Transmission

In the same file