Documentation

Lean 4 Proof

theorem laborShare_increases_with_kl_ratio_complements {α ρ : ℝ}
    (hα : 0 < α) (hα1 : α < 1) (hρ : ρ < 0)
    {K₁ K₂ L : ℝ} (hK₁ : 0 < K₁) (hK₂ : 0 < K₂) (hL : 0 < L)
    (hK : K₁ < K₂) :
    laborShare α ρ K₁ L < laborShare α ρ K₂ L := by
  simp only [laborShare, cesInner]
  -- s_L = (1-α)L^ρ / (αK^ρ + (1-α)L^ρ)
  -- When ρ < 0: K₁ < K₂ implies K₁^ρ > K₂^ρ (rpow reverses for neg exponent)
  -- So denominator₁ > denominator₂, same numerator → s_L(K₁) < s_L(K₂) ✓
  have h1α : (0 : ℝ) < 1 - α := by linarith
  have hnum : 0 < (1 - α) * L ^ ρ := mul_pos h1α (rpow_pos_of_pos hL ρ)
  have hd1 : 0 < α * K₁ ^ ρ + (1 - α) * L ^ ρ :=
    add_pos (mul_pos hα (rpow_pos_of_pos hK₁ ρ)) hnum
  have hd2 : 0 < α * K₂ ^ ρ + (1 - α) * L ^ ρ :=
    add_pos (mul_pos hα (rpow_pos_of_pos hK₂ ρ)) hnum
  apply div_lt_div_of_pos_left hnum hd2
  -- Need: α*K₂^ρ + (1-α)*L^ρ < α*K₁^ρ + (1-α)*L^ρ
  -- i.e., K₂^ρ < K₁^ρ (for ρ < 0, K₁ < K₂)
  have hKρ : K₂ ^ ρ < K₁ ^ ρ :=
    (Real.rpow_lt_rpow_iff_of_neg hK₂ hK₁ hρ).mpr hK
  linarith [mul_lt_mul_of_pos_left hKρ hα]

Dependency Graph

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:438

Module Section

Two-Factor CES Production Function (Layer 1 of Macro Extension)

In the same file