Documentation

Lean 4 Proof

theorem dtcPremium_exponent {α ρ σ A_K K A_L L : ℝ}
    (_hα : 0 < α) (_hα1 : α < 1) (hρ1 : ρ ≠ 1)
    (hK : 0 < K) (hL : 0 < L)
    (hσ : σ = 1 / (1 - ρ))
    (hbias : A_K / A_L = (K / L) ^ (σ - 1)) :
    relativeWageDTC α ρ A_K K A_L L = (α / (1 - α)) * (K / L) ^ (σ - 2) := by
  simp only [relativeWageDTC]
  -- Substitute the bias condition A_K/A_L = (K/L)^{σ-1}
  rw [hbias]
  -- Combine ((K/L)^{σ-1})^ρ into (K/L)^{(σ-1)·ρ}
  rw [← rpow_mul (le_of_lt (div_pos hK hL))]
  -- Reassociate to combine rpow terms
  rw [mul_assoc, ← rpow_add (div_pos hK hL)]
  -- Reduce exponent identity: (σ-1)·ρ + (ρ-1) = σ-2
  congr 1; congr 1
  subst hσ
  have h1ρ : (1 : ℝ) - ρ ≠ 0 := sub_ne_zero.mpr (Ne.symm hρ1)
  field_simp
  ring

Dependency Graph

Location

thesis/CESProofs/Macro/DirectedTechnicalChange.lean:189

Module Section

Directed Technical Change Extension (Acemoglu 2002)

In the same file