Documentation

Lean 4 Proof

theorem euler_factorAugmented {α ρ 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) :
    mpkFactorAugmented α ρ A_K K A_L L * K +
    mplFactorAugmented α ρ A_K K A_L L * L =
    factorAugmentedCES α ρ A_K K A_L L := by
  simp only [mpkFactorAugmented, mplFactorAugmented]
  rw [factorAugmentedCES_eq_twoFactorCES]
  rw [show A_K * marginalProductK 1 α ρ (A_K * K) (A_L * L) * K =
      marginalProductK 1 α ρ (A_K * K) (A_L * L) * (A_K * K) from by ring,
      show A_L * marginalProductL 1 α ρ (A_K * K) (A_L * L) * L =
      marginalProductL 1 α ρ (A_K * K) (A_L * L) * (A_L * L) from by ring]
  exact euler_two_factor one_pos hα hα1 hρ (mul_pos hAK hK) (mul_pos hAL hL)

Dependency Graph

Location

thesis/CESProofs/Macro/DirectedTechnicalChange.lean:109

Module Section

Directed Technical Change Extension (Acemoglu 2002)

In the same file