Documentation

Lean 4 Proof

theorem currency_union_maximizes_Keff (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {Tstar : ℝ} (hTs : 0 < Tstar) :
    effectiveCurvatureKeff J ρ 0 Tstar = curvatureK J ρ :=
  effectiveCurvatureKeff_zero_friction J ρ Tstar hTs

Dependency Graph

Location

thesis/CESProofs/Applications/OpenEconomy.lean:111

Module Section

Open Economy Monetary Transmission

In the same file