Documentation

Lean 4 Proof

theorem factorShare_identity {α ρ K L : ℝ}
    (hα : 0 < α) (hα1 : α < 1) (hK : 0 < K) (hL : 0 < L) :
    Real.log (laborShare α ρ K L / capitalShare α ρ K L) =
    Real.log ((1 - α) / α) + ρ * Real.log (L / K) := by
  simp only [laborShare, capitalShare, cesInner]
  set I := α * K ^ ρ + (1 - α) * L ^ ρ
  have hI_ne : I ≠ 0 := ne_of_gt (cesInner_pos hα hα1 hK hL)
  -- s_L/s_K = [(1-α)L^ρ/I] / [αK^ρ/I] = (1-α)L^ρ / (αK^ρ)
  have hαKρ : 0 < α * K ^ ρ := mul_pos hα (rpow_pos_of_pos hK ρ)
  rw [show (1 - α) * L ^ ρ / I / (α * K ^ ρ / I) =
      (1 - α) * L ^ ρ / (α * K ^ ρ) from by field_simp]
  -- (1-α)L^ρ / (αK^ρ) = [(1-α)/α] · (L/K)^ρ
  rw [show (1 - α) * L ^ ρ / (α * K ^ ρ) =
      ((1 - α) / α) * (L ^ ρ / K ^ ρ) from by field_simp]
  rw [← div_rpow (le_of_lt hL) (le_of_lt hK)]
  rw [Real.log_mul (ne_of_gt (div_pos (by linarith) hα))
      (ne_of_gt (rpow_pos_of_pos (div_pos hL hK) ρ))]
  rw [Real.log_rpow (div_pos hL hK)]

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:306

Module Section

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

In the same file