Documentation

Lean 4 Proof

theorem factorAugmentedCES_crs {α ρ 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) {c : ℝ} (hc : 0 < c) :
    factorAugmentedCES α ρ A_K (c * K) A_L (c * L) =
    c * factorAugmentedCES α ρ A_K K A_L L := by
  rw [factorAugmentedCES_eq_twoFactorCES, factorAugmentedCES_eq_twoFactorCES]
  rw [show A_K * (c * K) = c * (A_K * K) from by ring,
      show A_L * (c * L) = c * (A_L * L) from by ring]
  exact twoFactorCES_homogDegOne one_pos hα hα1 hρ
    (mul_pos hAK hK) (mul_pos hAL hL) hc

Dependency Graph

Location

thesis/CESProofs/Macro/DirectedTechnicalChange.lean:95

Module Section

Directed Technical Change Extension (Acemoglu 2002)

In the same file