theorem substitutability_dampens_inequality {ρ r : ℝ}
    (hρ_lt : ρ < 1) (hr : 1 < r) :
    r ^ ρ < r := by
  conv_rhs => rw [← rpow_one r]
  exact rpow_lt_rpow_of_exponent_lt (by linarith) hρ_lt

theorem piketty_r_gt_g {r g s_K s δ : ℝ}
    (hδ : 0 < δ) (hs : 0 < s)
    (h_solow : s_K = r * s / δ) :
    r > g ↔ s_K > g * s / δ := by
  subst h_solow
  constructor
  · intro h
    exact div_lt_div_of_pos_right (mul_lt_mul_of_pos_right h hs) hδ
  · intro h
    rw [gt_iff_lt] at h ⊢
    by_contra h_neg
    push_neg at h_neg
    have : r * s ≤ g * s := mul_le_mul_of_nonneg_right h_neg (le_of_lt hs)
    have : r * s / δ ≤ g * s / δ := div_le_div_of_nonneg_right this (le_of_lt hδ)
    linarith

theorem atkinsonIndex_nonneg_equal_weights (J : ℕ) (hJ : 0 < J)
    {ρ : ℝ} (hρ_pos : 0 < ρ) (hρ_lt : ρ < 1)
    (c : Fin J → ℝ) (hc : ∀ j, 0 < c j) :
    -- Power mean of order ρ ≤ arithmetic mean (power mean inequality)
    powerMean J ρ (ne_of_gt hρ_pos) c ≤ (1 / ↑J) * ∑ j : Fin J, c j := by
  exact powerMean_le_arithMean hρ_pos hρ_lt.le (ne_of_gt hρ_pos) (fun j => (hc j).le) hJ

theorem atkinson_index_nonneg_equal_weights (J : ℕ) (hJ : 0 < J)
    {ρ : ℝ} (hρ_pos : 0 < ρ) (hρ_lt : ρ < 1)
    (c : Fin J → ℝ) (hc : ∀ j, 0 < c j) :
    -- Power mean of order ρ ≤ arithmetic mean (power mean inequality)
    powerMean J ρ (ne_of_gt hρ_pos) c ≤ (1 / ↑J) * ∑ j : Fin J, c j := by
  exact powerMean_le_arithMean hρ_pos hρ_lt.le (ne_of_gt hρ_pos) (fun j => (hc j).le) hJ

theorem herfindahl_entry_decrease (J : ℕ) (hJ : 0 < J) :
    equalWeightH (J + 1) < equalWeightH J := by
  simp only [equalWeightH]
  apply div_lt_div_of_pos_left one_pos
  · exact_mod_cast hJ
  · norm_cast
    omega

theorem merger_reduces_curvature {ρ a_i a_j : ℝ}
    (hρ : ρ < 1) (hi : 0 < a_i) (hj : 0 < a_j) :
    -- Curvature change from merger: ΔK = -(1-ρ)·ΔH = -(1-ρ)·2aᵢaⱼ < 0
    (1 - ρ) * (2 * a_i * a_j) > 0 := by
  apply mul_pos (by linarith) (by positivity)

theorem impossible_trinity {T_home T_foreign T_capital T_trade : ℝ}
    (h_total : totalBilateralFriction T_home T_foreign T_capital T_trade = 0)
    (h_cap : 0 ≤ T_capital) (h_trade : 0 ≤ T_trade) :
    T_home = T_foreign := by
  simp only [totalBilateralFriction] at h_total
  have h1 : |T_home - T_foreign| = 0 := by linarith [abs_nonneg (T_home - T_foreign)]
  linarith [abs_eq_zero.mp h1]