Documentation

Lean 4 Proof

theorem factorShare_identity_augmented {α ρ A_K K A_L L : ℝ}
    (hα : 0 < α) (hα1 : α < 1)
    (hAK : 0 < A_K) (hK : 0 < K) (hAL : 0 < A_L) (hL : 0 < L) :
    Real.log (laborShare α ρ (A_K * K) (A_L * L) /
              capitalShare α ρ (A_K * K) (A_L * L)) =
    Real.log ((1 - α) / α) + ρ * Real.log (A_L * L / (A_K * K)) :=
  factorShare_identity hα hα1 (mul_pos hAK hK) (mul_pos hAL hL)

Dependency Graph

Location

thesis/CESProofs/Macro/DirectedTechnicalChange.lean:284

Module Section

Directed Technical Change Extension (Acemoglu 2002)

In the same file