def relativeWageDTC (α ρ A_K K A_L L : ℝ) : ℝ := (α / (1 - α)) * (A_K / A_L) ^ ρ * (K / L) ^ (ρ - 1)
thesis/CESProofs/Macro/DirectedTechnicalChange.lean:52
Directed Technical Change Extension (Acemoglu 2002)