Documentation

Lean 4 Proof

theorem hub_reform_benefits_all_spokes {J : ℕ} (hJ : 2 ≤ J)
    {ρ : ℝ} (hρ : ρ < 1)
    {T : ℝ} (hT : 0 ≤ T)
    {Tstar_old Tstar_new : ℝ} (hOld : 0 < Tstar_old) (hNew : 0 < Tstar_new)
    (h_reform : Tstar_old ≤ Tstar_new) :
    effectiveCurvatureKeff J ρ T Tstar_old ≤ effectiveCurvatureKeff J ρ T Tstar_new :=
  institutional_amplification hJ hρ hOld hNew h_reform hT

Dependency Graph

Location

thesis/CESProofs/Applications/OpenEconomy.lean:189

Module Section

Open Economy Monetary Transmission

In the same file