Sections / Section 17: Welfare, Trade, Applications / monetary_divergence_symmetric

Monetary Divergence Symmetric

theoremprovedCurvature Roles

Documentation

Lean 4 Proof

theorem monetary_divergence_symmetric (T_h T_f : ℝ) :
    monetaryDivergenceFriction T_h T_f = monetaryDivergenceFriction T_f T_h := by
  simp only [monetaryDivergenceFriction, abs_sub_comm]

Dependency Graph

Location

thesis/CESProofs/Applications/OpenEconomy.lean:223

Module Section

Open Economy Monetary Transmission

In the same file

monetaryDivergenceFriction totalBilateralFriction 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