Total Bilateral Friction

def proved Curvature Roles

Documentation

Lean 4 Proof

def totalBilateralFriction (T_home T_foreign T_capital T_trade : ℝ) : ℝ :=
  |T_home - T_foreign| + T_capital + T_trade

Dependency Graph

Used by

impossible_trinity

Location

thesis/CESProofs/Applications/OpenEconomy.lean:44

Module Section

Open Economy Monetary Transmission

In the same file

monetaryDivergenceFriction tradeWeightedResponse divergence_raises_bilateral_friction common_policy_zero_friction impossible_trinity currency_union_maximizes_Keff spillover_stronger_for_complements institutions_dampen_spillover trade_weighted_response_bounded hub_reform_benefits_all_spokes spectral_gap_convergence spectralGap_convergence monetary_divergence_symmetric