Documentation

Lean 4 Proof

theorem capital_labor_demand_ratio {A α ρ K L : ℝ} (_hA : 0 < A)
    (hα : 0 < α) (hα1 : α < 1) (_hρ : ρ ≠ 0) (hρ1 : ρ ≠ 1)
    (hK : 0 < K) (hL : 0 < L) :
    K / L = (α / (1 - α)) ^ elasticityOfSubstitution ρ *
    (marginalProductL A α ρ K L / marginalProductK A α ρ K L) ^
      elasticityOfSubstitution ρ := by
  -- From mp_ratio: MPK/MPL = [α/(1-α)] · (K/L)^{ρ-1}
  -- So (K/L)^{ρ-1} = [MPK/MPL] · [(1-α)/α]
  -- K/L = {[MPK/MPL] · [(1-α)/α]}^{1/(ρ-1)}
  --     = {[(1-α)/α] · [MPK/MPL]}^{-σ}
  --     = [α/(1-α)]^σ · [MPL/MPK]^σ
  -- Proof: Use mp_ratio to express MPL/MPK, then simplify rpow chain.
  have hI := cesInner_pos (ρ := ρ) hα hα1 hK hL
  have h1α : (0 : ℝ) < 1 - α := by linarith
  have hLK : 0 < L / K := div_pos hL hK
  have hαr : 0 < α / (1 - α) := div_pos hα h1α
  have h_inv : 0 < (1 - α) / α := div_pos h1α hα
  have hIr := rpow_pos_of_pos hI ((1 - ρ) / ρ)
  -- Unfold definitions to expose the algebraic structure
  simp only [elasticityOfSubstitution, marginalProductK, marginalProductL]
  have h1 : A * (1 - α) * L ^ (ρ - 1) * cesInner α ρ K L ^ ((1 - ρ) / ρ) /
      (A * α * K ^ (ρ - 1) * cesInner α ρ K L ^ ((1 - ρ) / ρ)) =
      (1 - α) * L ^ (ρ - 1) / (α * K ^ (ρ - 1)) := by
    have ha : A * (1 - α) * L ^ (ρ - 1) * cesInner α ρ K L ^ ((1 - ρ) / ρ) =
      ((1 - α) * L ^ (ρ - 1)) * (A * cesInner α ρ K L ^ ((1 - ρ) / ρ)) := by ring
    have hb : A * α * K ^ (ρ - 1) * cesInner α ρ K L ^ ((1 - ρ) / ρ) =
      (α * K ^ (ρ - 1)) * (A * cesInner α ρ K L ^ ((1 - ρ) / ρ)) := by ring
    rw [ha, hb]; exact mul_div_mul_right _ _ (ne_of_gt (mul_pos _hA hIr))
  rw [h1]
  -- Step 2: Rewrite as ((1-α)/α) * (L/K)^(ρ-1)
  have h2 : (1 - α) * L ^ (ρ - 1) / (α * K ^ (ρ - 1)) =
      ((1 - α) / α) * (L / K) ^ (ρ - 1) := by
    rw [div_rpow (le_of_lt hL) (le_of_lt hK), mul_div_mul_comm]
  rw [h2]
  -- Step 3: Distribute rpow over product
  rw [mul_rpow (le_of_lt h_inv) (rpow_nonneg (le_of_lt hLK) (ρ - 1))]
  -- Step 4: Weight cancellation: (α/(1-α))^σ * ((1-α)/α)^σ = 1
  have h_wt : (α / (1 - α)) ^ (1 / (1 - ρ)) * ((1 - α) / α) ^ (1 / (1 - ρ)) = 1 := by
    rw [← mul_rpow (le_of_lt hαr) (le_of_lt h_inv)]
    rw [div_mul_div_comm, mul_comm α (1 - α), div_self (ne_of_gt (mul_pos h1α hα))]
    exact one_rpow _
  rw [← mul_assoc, h_wt, one_mul]
  -- Step 5: Combine exponents: ((L/K)^(ρ-1))^(1/(1-ρ)) = (L/K)^(-1) = K/L
  rw [← rpow_mul (le_of_lt hLK)]
  have hexp : (ρ - 1) * (1 / (1 - ρ)) = -1 := by
    have : (1 : ℝ) - ρ ≠ 0 := sub_ne_zero.mpr (Ne.symm hρ1)
    field_simp; ring
  rw [hexp, rpow_neg_one (L / K), inv_div]

Dependency Graph

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:480

Module Section

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

In the same file