Documentation

Lean 4 Proof

theorem factorAugmentedCES_eq_twoFactorCES {α ρ A_K K A_L L : ℝ} :
    factorAugmentedCES α ρ A_K K A_L L = twoFactorCES 1 α ρ (A_K * K) (A_L * L) := by
  simp only [factorAugmentedCES, twoFactorCES, factorAugmentedInner, cesInner, one_mul]

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/DirectedTechnicalChange.lean:77

Module Section

Directed Technical Change Extension (Acemoglu 2002)

In the same file