Documentation

Lean 4 Proof

theorem spillover_stronger_for_complements {J : ℕ} (hJ : 2 ≤ J)
    {ρ1 ρ2 : ℝ} (hρ : ρ1 < ρ2)
    {T_new T_old Tstar : ℝ} (hTs : 0 < Tstar) (h : T_new ≤ T_old) :
    policyResponse J ρ2 T_new T_old Tstar ≤
    policyResponse J ρ1 T_new T_old Tstar :=
  monetary_transmission_ordering hJ hρ hTs h

Dependency Graph

Location

thesis/CESProofs/Applications/OpenEconomy.lean:127

Module Section

Open Economy Monetary Transmission

In the same file