def factorAugmentedCES (α ρ A_K K A_L L : ℝ) : ℝ := (factorAugmentedInner α ρ A_K K A_L L) ^ (1 / ρ)
thesis/CESProofs/Macro/DirectedTechnicalChange.lean:36
Directed Technical Change Extension (Acemoglu 2002)