Trade Collapse At Critical

theorem proved CES Potential

Documentation

Lean 4 Proof

theorem trade_collapse_at_critical {J : ℕ} {ρ : ℝ}
    {T Tstar : ℝ} (hTs : 0 < Tstar) (hT : Tstar ≤ T) :
    effectiveCurvatureKeff J ρ T Tstar = 0 :=
  effectiveCurvatureKeff_above_critical J ρ T Tstar hTs hT

Dependency Graph

Location

thesis/CESProofs/Potential/BilateralTrade.lean:90

Module Section

Bilateral Trade Collapse Ordering

In the same file

bilateral_Keff_decreasing bilateral_Keff_strict bilateral_Keff_sq_decreasing diversification_degradation_ratio curvatureK_decreasing_in_rho complementary_goods_more_fragile complementary_goods_higher_Keff highest_friction_pair_fails_first efficiency_fragility_tradeoff noise_tolerance_increasing_in_rho