theorem factorAugmentedInner_eq_cesInner {α ρ A_K K A_L L : ℝ} : factorAugmentedInner α ρ A_K K A_L L = cesInner α ρ (A_K * K) (A_L * L) := rfl
thesis/CESProofs/Macro/DirectedTechnicalChange.lean:73
Directed Technical Change Extension (Acemoglu 2002)