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

Trade Weighted Response

defprovedCurvature Roles

Documentation

Lean 4 Proof

def tradeWeightedResponse (N : ℕ) (w response : Fin N → ℝ) : ℝ :=
  ∑ j : Fin N, w j * response j

Dependency Graph

Used by

trade_weighted_response_bounded

Location

thesis/CESProofs/Applications/OpenEconomy.lean:50

Module Section

Open Economy Monetary Transmission

In the same file

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