Documentation

Lean 4 Proof

theorem relativeWage_formula {α ρ A_K K A_L L : ℝ}
    (hα : 0 < α) (hα1 : α < 1) {_hρ : ρ ≠ 0}
    (hAK : 0 < A_K) (hAL : 0 < A_L) (hK : 0 < K) (hL : 0 < L) :
    mpkFactorAugmented α ρ A_K K A_L L / mplFactorAugmented α ρ A_K K A_L L =
    relativeWageDTC α ρ A_K K A_L L := by
  simp only [mpkFactorAugmented, mplFactorAugmented]
  have hAKK := mul_pos hAK hK
  have hALL := mul_pos hAL hL
  -- Step 1: Factor a*b/(c*d) = (a/c)*(b/d)
  rw [mul_div_mul_comm]
  -- Step 2: Apply mp_ratio for effective inputs
  have h_mp := @mp_ratio 1 α ρ (A_K * K) (A_L * L) one_pos hα hα1 _hρ hAKK hALL
  rw [h_mp]
  -- Goal: A_K/A_L * ((α/(1-α)) * ((A_K*K)/(A_L*L))^{ρ-1}) = relativeWageDTC ...
  simp only [relativeWageDTC]
  -- Step 3: Decompose (A_K*K)/(A_L*L) = (A_K/A_L) * (K/L)
  rw [mul_div_mul_comm A_K K A_L L]
  -- Step 4: Distribute rpow over product
  rw [mul_rpow (le_of_lt (div_pos hAK hAL)) (le_of_lt (div_pos hK hL))]
  -- Step 5: Rearrange and combine A_K/A_L * (A_K/A_L)^{ρ-1} = (A_K/A_L)^ρ
  rw [show A_K / A_L * (α / (1 - α) * ((A_K / A_L) ^ (ρ - 1) * (K / L) ^ (ρ - 1))) =
      α / (1 - α) * (A_K / A_L * (A_K / A_L) ^ (ρ - 1)) * (K / L) ^ (ρ - 1) from by ring]
  rw [rpow_succ_pred (div_pos hAK hAL) ρ]

Dependency Graph

Location

thesis/CESProofs/Macro/DirectedTechnicalChange.lean:141

Module Section

Directed Technical Change Extension (Acemoglu 2002)

In the same file