Sections / Section 9: CES Potential and Information Friction / curvatureK_decreasing_in_rho

Curvature K Decreasing In Rho

theoremprovedCES Potential

Documentation

Lean 4 Proof

theorem curvatureK_decreasing_in_rho {J : ℕ} (hJ : 2 ≤ J)
    {rho1 rho2 : ℝ} (hrho : rho1 < rho2) :
    curvatureK J rho2 < curvatureK J rho1 := by
  simp only [curvatureK]
  apply div_lt_div_of_pos_right _ (by exact_mod_cast (show 0 < J by omega))
  exact mul_lt_mul_of_pos_right (by linarith) (by
    have : (2 : ℝ) ≤ ↑J := by exact_mod_cast hJ
    linarith)

Dependency Graph

Used by

complementary_sectors_highest_return complementary_goods_higher_Keff cesMultiplier_decreasing_in_rho efficiency_volatility_tradeoff monetary_transmission_ordering multiplier_rho_ordering complementary_goods_more_fragile

Location

thesis/CESProofs/Potential/BilateralTrade.lean:102

Module Section

Bilateral Trade Collapse Ordering

In the same file

bilateral_Keff_decreasing bilateral_Keff_strict bilateral_Keff_sq_decreasing diversification_degradation_ratio trade_collapse_at_critical complementary_goods_more_fragile complementary_goods_higher_Keff highest_friction_pair_fails_first efficiency_fragility_tradeoff noise_tolerance_increasing_in_rho